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)))`