[I'll eventually write a version which begins by explaining free theorems, but for now here's a proof for the cognoscenti]

Consider an agda expression, any typed agda expression whose type is a `Set1`. Here are two examples, including one using dependent types.

id : {a : Set} → a → a id x = x ff : {a : Set} → {s : a → a} → (F : a → Set) → (f : {x : a} → F x → F (s x)) → {x : a} → (y : F x) → F (s (s x)) ff F f y = f (f y)

It is very straightforward to obtain a term, `ff₁`, which has the same type except that `Set` has been upgraded to a `Set1`. In fact, the expression `ff` already has the desired type, we just need to change its type annotation.

id₁ : {a : Set1} → a → a id₁ x = x ff₁ : {a : Set1} → {s : a → a} → (F : a → Set1) → (f : {x : a} → (F x) → (F (s x))) → {x : a} → (y : (F x)) → (F (s (s x))) ff₁ F f y = f (f y)

Now, let's make this change a bit more generic. Instead of fixing `Set1`, let's use an abstract target, `Set#`. Now, since agda doesn't know that `Set#` is a member of the `Set` hierarchy, the validity of the expression `(x : a)` does not follow from the fact that `(a : Set#)`, as it would for `(a : Set)` or `(a : Set1)`. For this reason, it is necessary to introduce the abstract type transformer `(value# : Set# -> Set1)`, which inserts `Set#` into the type hierarchy.

It is very straightforward to obtain a term, `ff#`, which has the same type as `ff` except that `Set` has been upgraded to a `Set#` and `value#` has been inserted at the appropriate places. In fact, the expression `ff` already has the desired type, we again just need to change its type annotation.

id# : {a : Set#} → value# a → value# a id# x = x ff# : {a : Set#} → {s : value# a → value# a} → (F : value# a → Set#) → (f : {x : value# a} → value# (F x) → value# (F (s x))) → {x : value# a} → (y : value# (F x)) → value# (F (s (s x))) ff# F f y = f (f y)

And now the punchline is that `ff#` is precisely the proof of the free theorem for `ff`, using the following instantiations for `Set#` and `result#`.

record Set# : Set1 where field a : Set a' : Set a~ : a → a' → Set record value# (a# : Set#) : Set where open Set# a# field x : a x' : a' x~ : a~ x x'

Even more free theorems can be obtained by using other instantiations. Note that in the usual formulation of the parametricity result, the type of the free theorems are usually given in a much longer, record-free form where each field is expanded into an individual parameter. It is tedious, but straightforward to convert between the two representations.

## No comments:

Post a comment