6. The Small Print: Parametricity🔗

Quantifying over v is meant to stop a term from depending on which v it is given. That guarantee is parametricity: a polymorphic definition behaves the same way at every type.The word is Christopher Strachey's (1967); the relational formulation used below is John Reynolds' (1983). Philip Wadler's paper "Theorems for free!" (1989) made it popular with programmers. For many languages it is a theorem about the language, proved from outside. Lean's logic does not contain it, and classical reasoning can branch on which type a definition was handed. The interpretations of the "same" term can then disagree.Lean's logic includes the law of the excluded middle, so if v = Unit then … else … is allowed even though no program could decide it. Such definitions cannot be compiled, and are marked noncomputable.

namespace PHOAS
open Term'

open Classical in
noncomputable def chameleon : Term := fun v =>
  if v = Unit then two v else I v

This is an exotic term of a new kind: it does not inspect its argument, it inspects the type. Counting sees two; printing sees I. Lean needs a proof even that String ≠ Unit: if the two were equal, ▸ would carry "all Unit values are equal" over to String, giving "a" = "b".simp rewrites the goal with the listed definitions and lemmas, plus a standard set, until it closes.

theorem string_ne_unit : String ≠ Unit := by⊢ String ≠ Unit
  intro hh:String = Unit⊢ False
  have : ∀ a b : String, a = b :=
    h ▸ fun (_ _ : Unit) => rflh:String = Unitthis:∀ (a b : String), a = b⊢ False
  exact absurd (this "a" "b") (byh:String = Unitthis:∀ (a b : String), a = b⊢ ¬"a" = "b" decideAll goals completed! 🐙)

example : chameleon.count = 3 := by⊢ chameleon.count = 3
  simp [chameleon, Term.count, two, Term'.count]All goals completed! 🐙

example : chameleon.toNamed = .lam "x0" (.var "x0") := by⊢ chameleon.toNamed = Named.Term.lam "x0" (Named.Term.var "x0")
  simp [chameleon, Term.toNamed, Term'.toNamed, I,
    string_ne_unit]⊢ toString "x" ++ Nat.repr 0 = "x0"
  rflAll goals completed! 🐙

6.1. Well-Formedness🔗

The fix is to state the missing uniformity for each term, as a property we can prove, instead of expecting the type to guarantee it. Interpret the term at two variable types at once, and require the two results to have the same shape, with variables paired up by the binder that introduced them. This is Reynolds' relational parametricity in miniature: a relation between two instantiations that the term must respect. Γ lists the pairs of variables bound so far.An inductive … → Prop defines a relation by rules: each constructor is one way to establish it. Names such as Γ and b₁ that are used without being declared become implicit arguments.

inductive Term'.Equiv {v₁ v₂ : Type} :
    List (v₁ × v₂) → Term' v₁ → Term' v₂ → Prop
  | var : (x, y) ∈ Γ → Equiv Γ (var x) (var y)
  | lam : (∀ x y, Equiv ((x, y) :: Γ) (b₁ x) (b₂ y)) →
      Equiv Γ (lam b₁) (lam b₂)
  | app : Equiv Γ f₁ f₂ → Equiv Γ a₁ a₂ →
      Equiv Γ (app f₁ a₁) (app f₂ a₂)

def Term.Wf (e : Term) : Prop :=
  ∀ v₁ v₂, Term'.Equiv [] (e v₁) (e v₂)

Honest terms are well-formed by a proof that mirrors their shape:

theorem two_wf : two.Wf := fun _ _ =>
  .lam fun _ _ => .lam fun _ _ =>
    .app (.var (byx✝⁵:Typex✝⁴:Typex✝³:x✝⁵x✝²:x✝⁴x✝¹:x✝⁵x✝:x✝⁴⊢ (x✝³, x✝²) ∈ [(x✝¹, x✝), (x✝³, x✝²)] simpAll goals completed! 🐙))
      (.app (.var (byx✝⁵:Typex✝⁴:Typex✝³:x✝⁵x✝²:x✝⁴x✝¹:x✝⁵x✝:x✝⁴⊢ (x✝³, x✝²) ∈ [(x✝¹, x✝), (x✝³, x✝²)] simpAll goals completed! 🐙)) (.var (byx✝⁵:Typex✝⁴:Typex✝³:x✝⁵x✝²:x✝⁴x✝¹:x✝⁵x✝:x✝⁴⊢ (x✝¹, x✝) ∈ [(x✝¹, x✝), (x✝³, x✝²)] simpAll goals completed! 🐙)))

The chameleon is not:

theorem chameleon_not_wf : ¬ chameleon.Wf := by⊢ ¬chameleon.Wf
  intro hh:chameleon.Wf⊢ False
  have h := h Unit Stringh✝:chameleon.Wfh:Equiv [] (chameleon Unit) (chameleon String)⊢ False
  simp only [chameleon, `if_pos` has been deprecated: Use `ite_eq_left` insteadif_pos, `if_neg` has been deprecated: Use `ite_eq_right` insteadif_neg string_ne_unit,
    two, I] at hh✝:chameleon.Wfh:Equiv [] (lam fun f => lam fun x => (var f).app ((var f).app (var x))) (lam fun x => var x)⊢ False
  cases h with
  | lam h =>lamh✝:chameleon.Wfh:∀ (x : Unit) (y : String),
  Equiv [(x, y)] ((fun f => lam fun x => (var f).app ((var f).app (var x))) x) ((fun x => var x) y)⊢ False cases h () "x"All goals completed! 🐙

end PHOAS

Theorems that relate two interpretations, such as "printing then parsing gives back the term", need Wf as a hypothesis. Theorems that use a single interpretation do not, and the next chapters live entirely in that case.