* Unit 15 --- Soundness and Completeness of Algorithm W
:PROPERTIES:
:CUSTOM_ID: unit-15-soundness-and-completeness-of-algorithm-w
:END:
*Tutorial 2: PL Semantics in Lean* · [[../README.org][← Back to README]]

** Goals
:PROPERTIES:
:CUSTOM_ID: goals
:END:
- Prove that Algorithm W is *sound*: every inferred type is derivable in the declarative system
- Prove that Algorithm W is *complete*: every derivable type can be inferred (up to generalization)
- Understand the relationship between inference and declarative rules

** Sources
:PROPERTIES:
:CUSTOM_ID: sources
:END:
- [[https://www.jeffvaughan.net/docs/hmproof.pdf][Vaughan 2008, §4]]
- [[https://github.com/sdemos/type-inference][sdemos/type-inference]] =Soundness.lean=, =Completeness.lean=

** The Theorems
:PROPERTIES:
:CUSTOM_ID: the-theorems
:END:
*Soundness*: If =infer(Γ, e) = (S, τ)=, then =Γ ⊢ e : τ= declaratively.

*Completeness*: If =Γ ⊢ e : τ= declaratively, then there exists =S, τ'= such that
=infer(Γ, e) = (S, τ')= and =τ= is a substitution instance of =τ'= (i.e., W finds the /most general/ type).

** Exercises
:PROPERTIES:
:CUSTOM_ID: exercises
:END:
#+begin_src lean
open HMTyping
open MonoType

-- 15.1 — Soundness of Algorithm W
theorem soundness_W (Γ : HMEnv) (e : HMExpr) (S : Subst) (τ : MonoType) (counter : Nat)
    (h : inferW Γ e counter = some (S, τ, _)) :
    HMTyping (applySubstEnv S Γ) e {vars := [], body := τ} :=
  by
    induction e generalizing Γ S τ counter with
    | var i =>
        -- Case: variable lookup. Need to relate instantiated type scheme to declarative Var rule.
        sorry
    | lam body ih =>
        -- Case: lambda. Use the IH and the Abs rule.
        sorry
    | app f a ihf iha =>
        -- Case: application. The unification produces a substitution that makes types match.
        -- Need substitution composition lemmas.
        sorry
    | lett e₁ e₂ ih₁ ih₂ =>
        -- Case: let. Generalization produces a type scheme; the body gets the polymorphic type.
        sorry

-- 15.2 — Completeness of Algorithm W
theorem completeness_W (Γ : HMEnv) (e : HMExpr) (σ : TypeScheme)
    (h : HMTyping Γ e σ) :
    ∃ (S : Subst) (τ : MonoType) (counter : Nat),
      inferW Γ e 0 = some (S, τ, counter) ∧
      ∃ (S' : Subst), applySubst S' τ = σ.body :=
  by
    induction h with
    | var Γ i hlook =>
        sorry
    | abs Γ e τ₁ τ₂ hbody ih =>
        sorry
    | app Γ e₁ e₂ σ τ₁ τ₂ σ' h₁ h₂ h_eq ih₁ ih₂ =>
        sorry
    | lett Γ e₁ e₂ σ σ' τ h₁ h₂ ih₁ ih₂ =>
        sorry
    | gen Γ e σ αs hbody hfresh ih =>
        sorry
    | inst Γ e σ τ subst hbody hinst ih =>
        sorry

-- 15.3 — Principal Types Corollary
-- Every well-typed expression has a *principal type* — one that all others are instances of.
theorem principal_types (Γ : HMEnv) (e : HMExpr) (σ : TypeScheme)
    (h : HMTyping Γ e σ) :
    ∃ (τ_principal : MonoType),
      -- W finds the principal type
      (∃ S c, inferW Γ e 0 = some (S, τ_principal, c)) ∧
      -- σ's body is an instance of the principal type
      (∃ S', applySubst S' τ_principal = σ.body) :=
  by
    exact completeness_W Γ e σ h
#+end_src

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

← [[file:14-algorithm-w.org][Previous: Unit 14]] · [[file:.][← Tutorial 2 Index]] · [[../README.org][← Back to README]]