* Unit 13 --- Hindley-Milner Declarative Typing Rules
:PROPERTIES:
:CUSTOM_ID: unit-13-hindley-milner-declarative-typing-rules
:END:
*Tutorial 2: PL Semantics in Lean* · [[../README.org][← Back to README]]

** Goals
:PROPERTIES:
:CUSTOM_ID: goals
:END:
- Extend STLC with *let-polymorphism*
- Encode HM types with *type schemes* =∀α. τ=
- Formalize the 6 declarative typing rules (Var, App, Abs, Let, Inst, Gen)
- Understand the distinction between monomorphic (=τ=) and polymorphic (=σ = ∀α.τ=) types

** Sources
:PROPERTIES:
:CUSTOM_ID: sources
:END:
- [[https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system][Wikipedia: Hindley-Milner type system]]
- [[https://www.jeffvaughan.net/docs/hmproof.pdf][Vaughan 2008]] (declarative rules, §2)
- [[https://github.com/sdemos/type-inference][sdemos/type-inference]] (Lean formalization)

** Background
:PROPERTIES:
:CUSTOM_ID: background
:END:
HM adds *let-polymorphism* to STLC:

#+begin_example
let x = e₁ in e₂
#+end_example

In STLC, =x= would have a single monomorphic type. In HM, =x= gets a type
/scheme/ --- e.g., =∀α. α → α= for the identity function --- and each use of =x=
instantiates the scheme with fresh type variables.

The declarative rules:

#+begin_example
Var:    Γ, x:σ ⊢ x : σ
App:    Γ ⊢ e₁ : τ₁ → τ₂    Γ ⊢ e₂ : τ₁   ⇛   Γ ⊢ e₁ e₂ : τ₂
Abs:    Γ, x:τ₁ ⊢ e : τ₂   ⇛   Γ ⊢ λx.e : τ₁ → τ₂
Let:    Γ ⊢ e₁ : σ       Γ, x:σ ⊢ e₂ : τ   ⇛   Γ ⊢ let x = e₁ in e₂ : τ
Inst:   Γ ⊢ e : ∀α.τ   ⇛   Γ ⊢ e : τ[α := τ']
Gen:    Γ ⊢ e : τ   ∧   α ∉ ftv(Γ)   ⇛   Γ ⊢ e : ∀α.τ
#+end_example

** Exercises
:PROPERTIES:
:CUSTOM_ID: exercises
:END:
#+begin_src lean
-- 13.1 — Types and type schemes
inductive MonoType where
  | tvar  (id : Nat)              -- type variable α
  | fn    (τ₁ τ₂ : MonoType)      -- τ₁ → τ₂
deriving Repr, DecidableEq

notation:40 τ₁ " ⇒ " τ₂ => MonoType.fn τ₁ τ₂

-- A type scheme: ∀α₁...αₙ. τ  (quantified over a set of type variables)
structure TypeScheme where
  vars : List Nat               -- bound type variables
  body : MonoType
deriving Repr

-- 13.2 — HM expression syntax (extend STLC with `let`)
inductive HMExpr where
  | var (i : Nat)                -- de Bruijn index
  | lam (body : HMExpr)          -- λ. e
  | app (f a : HMExpr)           -- f a
  | lett (e₁ e₂ : HMExpr)        -- let x = e₁ in e₂
deriving Repr

-- 13.3 — Environments
-- Γ maps de Bruijn indices to type schemes
def HMEnv := List TypeScheme

-- 13.4 — Declarative typing rules
inductive HMTyping : HMEnv → HMExpr → TypeScheme → Prop where

  -- Var: look up variable in the environment
  | var (Γ : HMEnv) (i : Nat) (h : lookup Γ i = some σ) : HMTyping Γ (HMExpr.var i) σ

  -- Abs: λx. e  — note: x gets a monomorphic type in the lambda body
  | abs (Γ : HMEnv) (e : HMExpr) (τ₁ τ₂ : MonoType)
        (h : HMTyping ({vars := [], body := τ₁} :: Γ) e {vars := [], body := τ₂}) :
      HMTyping Γ (HMExpr.lam e) {vars := [], body := τ₁ ⇒ τ₂}

  -- App: e₁ e₂
  | app (Γ : HMEnv) (e₁ e₂ : HMExpr) (σ τ₁ τ₂ : MonoType) (σ' : TypeScheme)
        (h₁ : HMTyping Γ e₁ σ') (h₂ : HMTyping Γ e₂ {vars := [], body := τ₁})
        (h_eq : σ' = {vars := [], body := τ₁ ⇒ τ₂}) :
      HMTyping Γ (HMExpr.app e₁ e₂) {vars := [], body := τ₂}

  -- Let: e₁ is generalized and e₂ can use the polymorphic type
  | lett (Γ : HMEnv) (e₁ e₂ : HMExpr) (σ σ' : TypeScheme) (τ : MonoType)
        (h₁ : HMTyping Γ e₁ σ) (h₂ : HMTyping (σ :: Γ) e₂ σ') :
      HMTyping Γ (HMExpr.lett e₁ e₂) σ'

  -- Gen: generalize over free type variables not in the environment
  | gen (Γ : HMEnv) (e : HMExpr) (σ : TypeScheme) (αs : List Nat)
        (h : HMTyping Γ e σ) (hfresh : ∀ α, α ∈ αs → α ∉ ftv_env Γ) :
      HMTyping Γ e {σ with vars := αs ++ σ.vars}

  -- Inst: instantiate a type scheme
  | inst (Γ : HMEnv) (e : HMExpr) (σ : TypeScheme) (τ : MonoType) (subst : Nat → MonoType)
        (h : HMTyping Γ e σ) (hinst : apply_subst subst σ = τ) :
      HMTyping Γ e {vars := [], body := τ}

-- 13.5 — Exercise: the identity function is polymorphic
def id_type : TypeScheme := {vars := [0], body := MonoType.tvar 0 ⇒ MonoType.tvar 0}

theorem id_polymorphic : HMTyping [] (HMExpr.lam (HMExpr.var 0)) id_type :=
  by
    sorry

-- 13.6 — Exercise: let x = λy. y in x x  (instantiation of polymorphic identity)
-- This term should be well-typed — the identity is used at two different types
def self_app_id : HMExpr :=
  HMExpr.lett (HMExpr.lam (HMExpr.var 0)) (HMExpr.app (HMExpr.var 0) (HMExpr.var 0))

theorem self_app_id_typed (τ : MonoType) :
    HMTyping [] self_app_id {vars := [], body := τ ⇒ τ} :=
  by
    sorry
#+end_src

--------------

← [[file:12-type-safety.org][Previous: Unit 12]] · Next: [[file:14-algorithm-w.org][Unit 14 --- Algorithm W]]