At a high level:

• The policy is compiled to Minsicript.
• Miniscript is encoded to bitcoin Script. (One to One Mapping)
• Bitcoin Script is decoded back to Miniscript. (One to One Mapping)
• Policy and Miniscript can both be lifted to another representation for static analysis.

Following invariants are respected in Miniscript: Let ms be a miniscript, s be bitcoin script, pol be policy

• decode(encode(ms)) = ms
• encode(decode(s)) = s
• lift(pol) = lift(compile(pol))

I am not going into the details of lifting as it not directly related to the question.

When would I use policy language rather than Miniscript? What does policy language offer that Miniscript doesn't? What are the key differences between them?

I think this is question is best answered by an example.

Writing an efficient Miniscipt directly from spending conditions is not trivial. Policy language is a more natural way to write the spending conditions. Consider an Hashlock example from Bob to Alice, your requirements are

• Alice can spend the coins if they know a preimage for hash H
• Funds are sent back to Bob after some time T say 10 blocks

This naturally translates to following policy or(and(sha256(H),pk(A)),and(older(10),pk(B)))  . Writing a Miniscript for this directly would be complicated and probably would turn out to inefficient. This is where the compiler can help you.

The compiler would then compile down to a miniscript like the shown below. andor(c:pk(A),sha256(H),and_v(vc:pk(B),older(10))) which has a one to one mapping to script.

Note that it is non-trivial to directly write down this Miniscript and involves complicated fragments like andor.

The policy language additionally allows specifying the odds(by using @ as shown below) for a or branch which can help compiler produce vbyte efficient script. In the above example, we expect the Hashlock to succeed with high probability and the timelock branch should almost never be taken. We can use the odds in the policy language as follows:

or(99@and(sha256(H),pk(A)),1@and(older(10),pk(B)))

which then compiles down to a different miniscript(note that pk(B) changed to pk_h(B))

andor(c:pk(A),sha256(H),and_v(vc:pk_h(B),older(10)))

At a high level:

• The policy is compiled to Miniscript.
• Miniscript is encoded to Bitcoin Script. (One to One Mapping)
• Bitcoin Script is decoded back to Miniscript. (One to One Mapping)
• Policy and Miniscript can both be lifted to another representation for static analysis.

Following invariants are respected in Miniscript: 
Let ms be a miniscript, s be bitcoin script, pol be policy

• decode(encode(ms)) = ms
• encode(decode(s)) = s
• lift(pol) = lift(compile(pol))

I am not going into the details of lifting as it not directly related to the question.

When would I use policy language rather than Miniscript? What does policy language offer that Miniscript doesn't? What are the key differences between them?

I think this is question is best answered by an example.

Writing an efficient Miniscript directly from spending conditions is not trivial. Policy language is a more natural way to write the spending conditions. Consider a Hashlock example from Bob to Alice, your requirements are

• Alice can spend the coins if they know a preimage for hash H
• Funds are sent back to Bob after some time T, say 10 blocks

This naturally translates to the following policy: or(and(sha256(H),pk(A)),and(older(10),pk(B))). Writing a Miniscript for this directly would be complicated and probably would turn out to inefficient. This is where the compiler can help you.

The compiler would then compile down to a Miniscript like the shown below. andor(c:pk(A),sha256(H),and_v(vc:pk(B),older(10))) which has a one to one mapping to Script.

Note that it is non-trivial to directly write down this Miniscript and that it involves complicated fragments like andor.

The policy language additionally allows specifying the odds  (by using @ as shown below) for a or branch which can help the compiler produce vbyte efficient Script. In the above example, we expect the Hashlock to succeed with high probability and the timelock branch to be almost never taken. We can use the odds in the policy language as follows:

or(99@and(sha256(H),pk(A)),1@and(older(10),pk(B)))

which then compiles down to a different Miniscript (note that pk(B) changed to pk_h(B))

andor(c:pk(A),sha256(H),and_v(vc:pk_h(B),older(10)))