§ Theorems for free

These are personal notes I made of a custom notation for denoting the relations from the theorems for free paper. I developed the notation since I wanted to keep track of what types are floating around and what the relations are doing. We interpret types as sets. If elements belong to the relation, ie, if (a, a') ∈ R ⊂ AxA, we will denote this as a[A -R- A']a'. We will now write down some inference rules:
  1. We define ReflB as a[Bool ReflB Bool]a
  2. We define ReflI as i[Int ReflI Int]i
  3. The product of two relations [A R B], [X S Y] is called as RxS, and is defined as: (a,x)[AxX RxS BxY](b,y) iff: ∀ abxy, a[A R B]b ∧ x[X S Y]y.
  4. The list space of a [A R B] is called [A* [A R B] B*], and is defined as: la[A* [A R B] B*]lb iff: ∀ la lb, |la| = |lb| ∧ (∀ i, la[i][A R B]lb[i])
  5. The function space of two relations [A R B], [X S Y] is called [A->X R->S B->Y], and is defined as: f[A->X R->S B->Y]g iff: ∀ a b, a[A R B]b => f(a)[X S Y]g(b).
  6. The type family space of two relations is a function that takes a relation [A R B] and produces a new relation: g[FA | [A R B] | FB]h. The relation takes as parameter a relation [A R B]for each choice.
  7. The space of relations of ∀X.F(X) is a relation defined by: g[A->FA | ∀X.F(X) [FA [A R B] FB]| B->FB]h∀ A B R, (g A)[FA | [A R B] | FB](h B).

§ Parametricity theorem

The parametricity thm states that for all terms (r: R), we can deduce r[R rel(R) R]r where rel(R) is the relation that fits the type, and is derived from the above rules.

§ Parametricity for lists when the relation is a function:

The list space of a [A R B] is called [A* [A R B] B*], and is defined as: la[A* [A R B] B*]lb iff:
  • ∀ la lb, |la| = |lb| ∧ (∀ i, la[i][A R B]lb[i])
Now, let us take a special case where [A R B] is a function δ: A -> B. That is:
  • a[A R B]b iff δ(a) = b.
If this is the case, then we can simplify the math to be:
  • la[A* [A R B] B*]lb <=> ∀ la lb, |la| = |lb| ∧ (∀ i, la[i][A R B]lb[i])
  • la[A* [A R B] B*]lb <=> ∀ la lb, |la| = |lb| ∧ (∀ i, δ(la[i]) = lb[i]
  • la[A* [A R B] B*]lb <=> ∀ la lb, map δ la = lb

§ Parametricity to prove rearrangements

  • r[∀ X. X* -> X*]r
  • (r A)[A*->A* | [A*->A* [A R B] B*->B*] | B*->B*](r B)
  • as[A* [A R B] B*]bs => (r A as)[A* [A R B] B*](r B bs)
  • Pick [A R B] to be a function δ: A -> B. Ie, a[A R B]b iff δ(a) = b.
  • This lets us convert all occrences of α[A R B]ω into ω = δ(α).
  • Hence, as[A* [A R B] B*]bs becomes map δ as = bs.
  • Hence, (r A as)[A* [A R B] B*](r B bs) becomes map δ (r A as) = (r B bs)
  • In toto, this let us replace bs with map δ as. We derive:
  • map δ (r A as) = (r B bs)
  • map δ (r A as) = (r B (map δ as)
  • map δ . (r A) = (r B) . map δ
  • Replace bs[i] with δ(as[i])to get result: δ(r A as[i]) = r B δ(as[i]), which was indeed what we were looking for.

§ References