Hindley–Milner type inference

InductiveExpressions of the λ-calculus with let#✓fully proved

An expression is a variable \(x\), an application \(e_1\,e_2\), an abstraction \(\lambda x.\, e\), or a let-binding \(\mathsf{let}\ x = e_1\ \mathsf{in}\ e_2\), where \(e\), \(e_1\), \(e_2\) are expressions and variable names \(x\) are strings.

inductive Expr where
  | var (x : String)
  | app (e₁ e₂ : Expr)
  | lam (x : String) (e : Expr)
  | let_ (x : String) (e₁ e₂ : Expr)
  deriving DecidableEq, Repr

Used by 16

Used byHindley–Milner typing · let generalizes · Soundness of type inference for closed expressions · Soundness of Algorithm W · Typing inversion for variables · Type inference for closed expressions · Completeness of type inference for closed expressions · Type inference succeeds exactly on typable closed expressions · Principal types · The let rule under a type substitution · Typing is preserved in more general contexts · The abstraction \(\lambda f.\, f\, f\) has no type · Hindley–Milner typing is stable under type substitution · Algorithm W · Completeness of Algorithm W · Freshness invariants of Algorithm W

AbbreviationMonotypes#✓fully proved

A monotype over a set \(B\) of base types is a term over the constants \(B\): a type variable \(\alpha \in \mathbb{N}\), a base type \(b \in B\), or an arrow \(\tau_1 \to \tau_2\) of two monotypes (a binary node).

abbrev Ty (B : Type u) := Term B

Uses 1 · Used by 28

Statement usesTerms for unification

Used byEvaluation of a type scheme · Generalization of a monotype · Generalization depends only on the free variables of the context · Generalizing in a context with fewer free variables · Renaming step of the substitution lemma · Hindley–Milner typing · let generalizes · Soundness of type inference for closed expressions · Soundness of Algorithm W · Typing inversion for variables · Type inference for closed expressions · Completeness of type inference for closed expressions · Type inference succeeds exactly on typable closed expressions · Principal types · Instantiation of a type scheme · Instantiation commutes with substitution · The let rule under a type substitution · Typing is preserved in more general contexts · More general type scheme · No monotype is an arrow out of itself · The abstraction \(\lambda f.\, f\, f\) has no type · Contexts with the same lookups are related by generality · Hindley–Milner typing is stable under type substitution · Substituting into a generalization is more general · Monotypes as type schemes · Algorithm W · Completeness of Algorithm W · Freshness invariants of Algorithm W

AbbreviationType schemes#✓fully proved

A type scheme over base types \(B\) is a term over the constant set \(B \oplus \mathbb{N}\): its variables \(\alpha \in \mathbb{N}\) are the free type variables, a constant \(\mathrm{inl}\, b\) is the base type \(b \in B\), a constant \(\mathrm{inr}\, i\) is the bound variable \(i\), and a node of two schemes is an arrow.

abbrev Scheme (B : Type u) := Term (B ⊕ ℕ)

Uses 1 · Used by 39

Statement usesTerms for unification

Used byBound-variable supremum of a type scheme · Extending more general contexts by a binding · Typing context · Evaluation of a type scheme · Free type variables of a context · Free type variables depend only on visible bindings · Generalization of a monotype · Generalization depends only on the free variables of the context · Generalizing in a context with fewer free variables · Renaming step of the substitution lemma · Hindley–Milner typing · let generalizes · Soundness of type inference for closed expressions · Soundness of Algorithm W · Typing inversion for variables · Type inference for closed expressions · Completeness of type inference for closed expressions · Type inference succeeds exactly on typable closed expressions · Principal types · Instantiation of a type scheme · Instantiation commutes with substitution · The let rule under a type substitution · Context lookup · Substitutions agreeing on a context give the same lookups · Typing is preserved in more general contexts · More general type scheme · More general context · The abstraction \(\lambda f.\, f\, f\) has no type · Contexts with the same lookups are related by generality · Applying a type substitution to a context · Hindley–Milner typing is stable under type substitution · Applying a type substitution to a scheme · Substitution into a scheme depends only on its free variables · Substituting into a generalization is more general · Monotypes as type schemes · Free type variables of a name's visible scheme · Algorithm W · Completeness of Algorithm W · Freshness invariants of Algorithm W

DefinitionMonotypes as type schemes#✓fully proved

Every monotype \(\tau\) is read as the type scheme with no bound variables of the same shape: a type variable stays the same type variable, a base type \(b\) becomes the constant \(\mathrm{inl}\, b\), and an arrow \(\tau_1 \to \tau_2\) becomes the arrow of the images of \(\tau_1\) and \(\tau_2\).

def toScheme : Ty B → Scheme B
  | var x => var x
  | const b => const (Sum.inl b)
  | node l r => node (toScheme l) (toScheme r)

Uses 3 · Used by 18

Statement usesType schemes · Monotypes · Terms for unification

Used byGeneralization of a monotype · Generalization depends only on the free variables of the context · Generalizing in a context with fewer free variables · Renaming step of the substitution lemma · Hindley–Milner typing · let generalizes · Soundness of Algorithm W · Typing inversion for variables · Instantiation commutes with substitution · Typing is preserved in more general contexts · The abstraction \(\lambda f.\, f\, f\) has no type · Hindley–Milner typing is stable under type substitution · Applying a type substitution to a scheme · Substitution into a scheme depends only on its free variables · Substituting into a generalization is more general · Algorithm W · Completeness of Algorithm W · Freshness invariants of Algorithm W

DefinitionEvaluation of a type scheme#✓fully proved

Given maps \(f\) and \(g\) from natural numbers to monotypes over \(B\), a type scheme \(\sigma\) over \(B\) evaluates to the monotype obtained by replacing each free type variable \(x\) of \(\sigma\) by \(f(x)\) and each bound variable \(i\) by \(g(i)\), keeping every base type \(b\) unchanged. An arrow \(\sigma_1 \to \sigma_2\) evaluates to the arrow from the evaluation of \(\sigma_1\) to the evaluation of \(\sigma_2\).

def Scheme.eval (f g : ℕ → Ty B) : Scheme B → Ty B
  | var x => f x
  | const (Sum.inl b) => const b
  | const (Sum.inr i) => g i
  | node l r => node (Scheme.eval f g l) (Scheme.eval f g r)

Uses 3 · Used by 9

Statement usesType schemes · Monotypes · Terms for unification

Used byGeneralizing in a context with fewer free variables · Renaming step of the substitution lemma · let generalizes · Instantiation of a type scheme · Instantiation commutes with substitution · The abstraction \(\lambda f.\, f\, f\) has no type · Substituting into a generalization is more general · Completeness of Algorithm W · Freshness invariants of Algorithm W

DefinitionInstantiation of a type scheme#✓fully proved

Given monotypes \((t_i)_{i \in \mathbb{N}}\), the instance of a scheme \(\sigma\) at \((t_i)\) is the monotype obtained from \(\sigma\) by replacing each bound variable \(i\) by \(t_i\), keeping its free type variables and base types unchanged.

def Scheme.inst (ts : ℕ → Ty B) (σ : Scheme B) : Ty B := σ.eval Term.var ts

Uses 4 · Used by 16

Statement usesType schemes · Evaluation of a type scheme · Monotypes · Terms for unification

Used byGeneralizing in a context with fewer free variables · Renaming step of the substitution lemma · Hindley–Milner typing · let generalizes · Soundness of Algorithm W · Typing inversion for variables · Instantiation commutes with substitution · Typing is preserved in more general contexts · More general type scheme · The abstraction \(\lambda f.\, f\, f\) has no type · Contexts with the same lookups are related by generality · Hindley–Milner typing is stable under type substitution · Substituting into a generalization is more general · Algorithm W · Completeness of Algorithm W · Freshness invariants of Algorithm W

DefinitionApplying a type substitution to a scheme#✓fully proved

For a type substitution \(s\) and a type scheme \(\sigma\), \(s\sigma\) is the scheme obtained from \(\sigma\) by replacing every free type variable \(x\) with the monotype \(s(x)\), read as a scheme with no bound variables. The bound variables of \(\sigma\) are left unchanged.

def Scheme.substTy (s : Subst B) (σ : Scheme B) : Scheme B := σ.subst fun x ↦ toScheme (s x)

Uses 4 · Used by 13

Statement usesType schemes · Monotypes as type schemes · Substitution · Applying a substitution to a term

Used byRenaming step of the substitution lemma · Soundness of type inference for closed expressions · Soundness of Algorithm W · Completeness of type inference for closed expressions · Instantiation commutes with substitution · The let rule under a type substitution · Substitutions agreeing on a context give the same lookups · Applying a type substitution to a context · Hindley–Milner typing is stable under type substitution · Substitution into a scheme depends only on its free variables · Substituting into a generalization is more general · Completeness of Algorithm W · Freshness invariants of Algorithm W

TheoremInstantiation commutes with substitution#✓fully proved

For every type substitution \(s\), every scheme \(\sigma\) and all monotypes \((t_i)_{i \in \mathbb{N}}\), instantiating each bound variable \(i\) of \(s(\sigma)\) by \(s(t_i)\) gives \(s\) applied to the instance of \(\sigma\) at \((t_i)\). Here \(s\) acts on a scheme through its free type variables only.

theorem inst_substTy (s : Subst B) (ts : ℕ → Ty B) (σ : Scheme B) :
    (σ.substTy s).inst (fun i ↦ (ts i).subst s) = (σ.inst ts).subst s

Uses 9 · Used by 1

Statement usesType schemes · Instantiation of a type scheme · Applying a type substitution to a scheme · Monotypes · Substitution · Applying a substitution to a term

Proof usesEvaluation of a type scheme · Monotypes as type schemes · Terms for unification

Used byHindley–Milner typing is stable under type substitution

TheoremSubstitution into a scheme depends only on its free variables#✓fully proved

If two type substitutions \(s\) and \(t\) satisfy \(s(x) = t(x)\) for every free type variable \(x\) of a type scheme \(\sigma\), then applying \(s\) to \(\sigma\) gives the same scheme as applying \(t\).

theorem substTy_congr {s t : Subst B} {σ : Scheme B} (h : ∀ x ∈ σ.vars, s x = t x) :
    σ.substTy s = σ.substTy t

Uses 7 · Used by 1

Statement usesType schemes · Applying a type substitution to a scheme · Substitution · Terms for unification · Variables of a term

Proof usesMonotypes as type schemes · Substitution depends only on the variables of the term

Used bySubstitutions agreeing on a context give the same lookups

AbbreviationTyping context#✓fully proved

A typing context over base types \(B\) is a finite list of bindings \((x, \sigma)\), each pairing a name \(x\) (a string) with a type scheme \(\sigma\) over \(B\). A name may be bound more than once; the first binding of a name in the list is the visible one.

abbrev Ctx (B : Type u) := List (String × Scheme B)

Uses 1 · Used by 27

Statement usesType schemes

Used byExtending more general contexts by a binding · Free type variables of a context · Free type variables depend only on visible bindings · Generalization of a monotype · Generalization depends only on the free variables of the context · Generalizing in a context with fewer free variables · Renaming step of the substitution lemma · Hindley–Milner typing · let generalizes · Soundness of type inference for closed expressions · Soundness of Algorithm W · Typing inversion for variables · Completeness of type inference for closed expressions · The let rule under a type substitution · Context lookup · Substitutions agreeing on a context give the same lookups · Typing is preserved in more general contexts · More general context · The abstraction \(\lambda f.\, f\, f\) has no type · Contexts with the same lookups are related by generality · Applying a type substitution to a context · Hindley–Milner typing is stable under type substitution · Substituting into a generalization is more general · Free type variables of a name's visible scheme · Algorithm W · Completeness of Algorithm W · Freshness invariants of Algorithm W

DefinitionContext lookup#✓fully proved

The lookup of a name \(x\) in a typing context \(\Gamma\) is the scheme of the first binding of \(x\) in \(\Gamma\) (the visible one), or nothing if \(\Gamma\) has no binding of \(x\).

def Ctx.lookup : Ctx B → String → Option (Scheme B)
  | [], _ => none
  | (y, σ) :: Γ, x => if x = y then some σ else Ctx.lookup Γ x

Uses 2 · Used by 19

Statement usesTyping context · Type schemes

Used byExtending more general contexts by a binding · Free type variables depend only on visible bindings · Renaming step of the substitution lemma · Hindley–Milner typing · let generalizes · Soundness of Algorithm W · Typing inversion for variables · The let rule under a type substitution · Substitutions agreeing on a context give the same lookups · Typing is preserved in more general contexts · More general context · The abstraction \(\lambda f.\, f\, f\) has no type · Contexts with the same lookups are related by generality · Hindley–Milner typing is stable under type substitution · Substituting into a generalization is more general · Free type variables of a name's visible scheme · Algorithm W · Completeness of Algorithm W · Freshness invariants of Algorithm W

DefinitionFree type variables of a name's visible scheme#✓fully proved

For a typing context \(\Gamma\) and a name \(x\), this is the set of free type variables of the scheme that \(\Gamma\) binds to \(x\) (the first binding of \(x\) in \(\Gamma\)), or the empty set if \(\Gamma\) does not bind \(x\).

def Ctx.visibleVars (Γ : Ctx B) (x : String) : Finset ℕ :=
  match Γ.lookup x with
  | some σ => σ.vars
  | none => ∅

Uses 4 · Used by 9

Statement usesTyping context · Context lookup · Type schemes · Variables of a term

Used byFree type variables of a context · Free type variables depend only on visible bindings · Renaming step of the substitution lemma · Completeness of type inference for closed expressions · Substitutions agreeing on a context give the same lookups · Typing is preserved in more general contexts · Substituting into a generalization is more general · Completeness of Algorithm W · Freshness invariants of Algorithm W

DefinitionFree type variables of a context#✓fully proved

The free type variables of a typing context \(\Gamma\) are the type variables occurring free in the visible scheme of some name bound in \(\Gamma\).

A binding shadowed by an earlier binding of the same name does not count, so the free type variables of \(\Gamma\) depend only on the visible scheme of each name.

def Ctx.ftv (Γ : Ctx B) : Finset ℕ := (Γ.map Prod.fst).toFinset.biUnion Γ.visibleVars

Uses 3 · Used by 14

Statement usesTyping context · Free type variables of a name's visible scheme · Type schemes

Used byFree type variables depend only on visible bindings · Generalization of a monotype · Generalization depends only on the free variables of the context · Generalizing in a context with fewer free variables · Renaming step of the substitution lemma · let generalizes · Completeness of type inference for closed expressions · The let rule under a type substitution · Substitutions agreeing on a context give the same lookups · Typing is preserved in more general contexts · Hindley–Milner typing is stable under type substitution · Substituting into a generalization is more general · Completeness of Algorithm W · Freshness invariants of Algorithm W

TheoremFree type variables depend only on visible bindings#✓fully proved

If two typing contexts \(\Gamma\) and \(\Gamma'\) give every name \(x\) the same visible scheme (or both bind no scheme to \(x\)), then \(\Gamma\) and \(\Gamma'\) have the same free type variables.

theorem Ctx.ftv_congr {Γ Γ' : Ctx B} (h : ∀ x, Γ.lookup x = Γ'.lookup x) : Γ.ftv = Γ'.ftv

Uses 6 · Used by 1

Statement usesTyping context · Free type variables of a context · Context lookup · Type schemes

Proof usesFree type variables of a name's visible scheme · Variables of a term

Used byCompleteness of Algorithm W

DefinitionApplying a type substitution to a context#✓fully proved

For a type substitution \(s\) and a typing context \(\Gamma\), \(s\Gamma\) is the context obtained by applying \(s\) to the scheme of every binding of \(\Gamma\), keeping the names and their order.

def Ctx.subst (s : Subst B) (Γ : Ctx B) : Ctx B := Γ.map fun p ↦ (p.1, p.2.substTy s)

Uses 4 · Used by 11

Statement usesTyping context · Type schemes · Applying a type substitution to a scheme · Substitution

Used byRenaming step of the substitution lemma · Soundness of type inference for closed expressions · Soundness of Algorithm W · Completeness of type inference for closed expressions · The let rule under a type substitution · Substitutions agreeing on a context give the same lookups · Hindley–Milner typing is stable under type substitution · Substituting into a generalization is more general · Algorithm W · Completeness of Algorithm W · Freshness invariants of Algorithm W

TheoremSubstitutions agreeing on a context give the same lookups#✓fully proved

If two type substitutions \(s\) and \(t\) agree on every free type variable of a context \(\Gamma\), then for every name \(x\) the lookups of \(x\) in \(s(\Gamma)\) and in \(t(\Gamma)\) are equal: both give no scheme, or both give the same scheme.

theorem Ctx.lookup_subst_congr {s t : Subst B} {Γ : Ctx B} (h : ∀ x ∈ Γ.ftv, s x = t x)
    (x : String) : (Γ.subst s).lookup x = (Γ.subst t).lookup x

Uses 11 · Used by 3

Statement usesTyping context · Free type variables of a context · Context lookup · Applying a type substitution to a context · Type schemes · Substitution · Terms for unification

Proof usesFree type variables of a name's visible scheme · Applying a type substitution to a scheme · Substitution into a scheme depends only on its free variables · Variables of a term

Used byThe let rule under a type substitution · Hindley–Milner typing is stable under type substitution · Completeness of Algorithm W

DefinitionGeneralization of a monotype#✓fully proved

Given a typing context \(\Gamma\) and a monotype \(\tau\), the generalization of \(\tau\) with respect to \(\Gamma\) is the type scheme obtained from \(\tau\) by turning each type variable \(\alpha\) that is not free in \(\Gamma\) into the bound variable with index \(\alpha\), while type variables free in \(\Gamma\) stay free.

def gen (Γ : Ctx B) (τ : Ty B) : Scheme B :=
  (toScheme τ).subst fun x ↦ if x ∈ Γ.ftv then var x else const (Sum.inr x)

Uses 7 · Used by 15

Statement usesTyping context · Free type variables of a context · Type schemes · Monotypes · Monotypes as type schemes · Terms for unification · Applying a substitution to a term

Used byGeneralization depends only on the free variables of the context · Generalizing in a context with fewer free variables · Renaming step of the substitution lemma · Hindley–Milner typing · let generalizes · Soundness of Algorithm W · Typing inversion for variables · The let rule under a type substitution · Typing is preserved in more general contexts · The abstraction \(\lambda f.\, f\, f\) has no type · Hindley–Milner typing is stable under type substitution · Substituting into a generalization is more general · Algorithm W · Completeness of Algorithm W · Freshness invariants of Algorithm W

InductiveHindley–Milner typing#✓fully proved

The syntax-directed Damas–Milner typing relation \(\Gamma \vdash e : \tau\) between a context \(\Gamma\), an expression \(e\) and a monotype \(\tau\) is the least relation closed under the following rules, where \(\Gamma, x : \sigma\) is \(\Gamma\) extended by the binding \(x : \sigma\) in front.

• Variable: if the lookup of \(x\) in \(\Gamma\) gives the scheme \(\sigma\), then \(\Gamma \vdash x : \tau\) for every instance \(\tau\) of \(\sigma\), obtained by replacing each bound variable \(i\) of \(\sigma\) by a monotype \(t_i\).
• Application: if \(\Gamma \vdash e_1 : \tau_1 \to \tau_2\) and \(\Gamma \vdash e_2 : \tau_1\), then \(\Gamma \vdash e_1\, e_2 : \tau_2\).
• Abstraction: if \(\Gamma, x : \tau_1 \vdash e : \tau_2\), with \(\tau_1\) bound as a scheme without bound variables, then \(\Gamma \vdash \lambda x.\, e : \tau_1 \to \tau_2\).
• Let: if \(\Gamma \vdash e_1 : \tau_1\) and \(\Gamma, x : \mathrm{gen}_\Gamma(\tau_1) \vdash e_2 : \tau_2\), then \(\Gamma \vdash \mathtt{let}\ x = e_1\ \mathtt{in}\ e_2 : \tau_2\), where \(\mathrm{gen}_\Gamma(\tau_1)\) binds the type variables of \(\tau_1\) that are not free in \(\Gamma\).

inductive HasType : Ctx B → Expr → Ty B → Prop
  /-- A variable has every instance of its scheme. -/
  | var {Γ : Ctx B} {x : String} {σ : Scheme B} (ts : ℕ → Ty B) :
      Γ.lookup x = some σ → HasType Γ (.var x) (σ.inst ts)
  | app {Γ : Ctx B} {e₁ e₂ : Expr} {τ₁ τ₂ : Ty B} :
      HasType Γ e₁ (node τ₁ τ₂) → HasType Γ e₂ τ₁ → HasType Γ (.app e₁ e₂) τ₂
  /-- An abstraction binds a monotype. -/
  | lam {Γ : Ctx B} {x : String} {e : Expr} {τ₁ τ₂ : Ty B} :
      HasType ((x, toScheme τ₁) :: Γ) e τ₂ → HasType Γ (.lam x e) (node τ₁ τ₂)
  /-- `let` generalizes the type of the bound expression. -/
  | let_ {Γ : Ctx B} {x : String} {e₁ e₂ : Expr} {τ₁ τ₂ : Ty B} :
      HasType Γ e₁ τ₁ → HasType ((x, gen Γ τ₁) :: Γ) e₂ τ₂ → HasType Γ (.let_ x e₁ e₂) τ₂

Uses 9 · Used by 12

Statement usesTyping context · Context lookup · Expressions of the λ-calculus with let · Type schemes · Instantiation of a type scheme · Monotypes · Generalization of a monotype · Monotypes as type schemes · Terms for unification

Used bylet generalizes · Soundness of type inference for closed expressions · Soundness of Algorithm W · Typing inversion for variables · Completeness of type inference for closed expressions · Type inference succeeds exactly on typable closed expressions · Principal types · The let rule under a type substitution · Typing is preserved in more general contexts · The abstraction \(\lambda f.\, f\, f\) has no type · Hindley–Milner typing is stable under type substitution · Completeness of Algorithm W

DefinitionMore general type scheme#✓fully proved

A scheme \(\sigma'\) is more general than a scheme \(\sigma\) when every instance of \(\sigma\) is also an instance of \(\sigma'\) and every free type variable of \(\sigma'\) is a free type variable of \(\sigma\).

def Scheme.MoreGeneral (σ' σ : Scheme B) : Prop :=
  (∀ ts, ∃ ts', σ'.inst ts' = σ.inst ts) ∧ σ'.vars ⊆ σ.vars

Uses 4 · Used by 8

Statement usesType schemes · Instantiation of a type scheme · Monotypes · Variables of a term

Used byExtending more general contexts by a binding · Generalizing in a context with fewer free variables · Renaming step of the substitution lemma · Typing is preserved in more general contexts · More general context · Contexts with the same lookups are related by generality · Substituting into a generalization is more general · Completeness of Algorithm W

DefinitionMore general context#✓fully proved

A context \(\Gamma'\) is more general than a context \(\Gamma\) when the same names are visible in both and, for each such name \(x\), the visible scheme of \(x\) in \(\Gamma'\) is more general than its visible scheme in \(\Gamma\). Only lookups matter, so shadowed bindings play no role.

def Ctx.MoreGeneral (Γ' Γ : Ctx B) : Prop :=
  (∀ x σ, Γ.lookup x = some σ → ∃ σ', Γ'.lookup x = some σ' ∧ σ'.MoreGeneral σ) ∧
    ∀ x σ', Γ'.lookup x = some σ' → ∃ σ, Γ.lookup x = some σ ∧ σ'.MoreGeneral σ

Uses 4 · Used by 5

Statement usesTyping context · Context lookup · Type schemes · More general type scheme

Used byExtending more general contexts by a binding · The let rule under a type substitution · Typing is preserved in more general contexts · Contexts with the same lookups are related by generality · Hindley–Milner typing is stable under type substitution

TheoremContexts with the same lookups are related by generality#✓fully proved

If two typing contexts \(\Gamma'\) and \(\Gamma\) give the same lookup result for every name \(x\) (the same visible scheme, or none in both), then \(\Gamma'\) is more general than \(\Gamma\).

Since the hypothesis is symmetric, \(\Gamma\) is then also more general than \(\Gamma'\).

theorem Ctx.MoreGeneral.of_lookup_eq {Γ' Γ : Ctx B} (h : ∀ x, Γ'.lookup x = Γ.lookup x) :
    Γ'.MoreGeneral Γ

Uses 8 · Used by 3

Statement usesTyping context · More general context · Context lookup · Type schemes

Proof usesMore general type scheme · Instantiation of a type scheme · Monotypes · Variables of a term

Used byThe let rule under a type substitution · Hindley–Milner typing is stable under type substitution · Completeness of Algorithm W

TheoremExtending more general contexts by a binding#✓fully proved

Let \(\Gamma'\) and \(\Gamma\) be typing contexts such that \(\Gamma'\) is more general than \(\Gamma\), let \(x\) be a name, and let \(\sigma'\) and \(\sigma\) be type schemes such that \(\sigma'\) is more general than \(\sigma\). Then the context obtained by putting the binding \(x : \sigma'\) in front of \(\Gamma'\) is more general than the context obtained by putting the binding \(x : \sigma\) in front of \(\Gamma\).

theorem Ctx.MoreGeneral.cons {Γ' Γ : Ctx B} (h : Γ'.MoreGeneral Γ) (x : String)
    {σ' σ : Scheme B} (hσ : σ'.MoreGeneral σ) :
    Ctx.MoreGeneral ((x, σ') :: Γ') ((x, σ) :: Γ)

Uses 5 · Used by 4

Statement usesTyping context · More general context · Type schemes · More general type scheme

Proof usesContext lookup

Used byThe let rule under a type substitution · Typing is preserved in more general contexts · Hindley–Milner typing is stable under type substitution · Completeness of Algorithm W

TheoremGeneralizing in a context with fewer free variables#✓fully proved

Let \(\Gamma'\) and \(\Gamma\) be typing contexts such that every free type variable of \(\Gamma'\) is a free type variable of \(\Gamma\), and let \(\tau\) be a monotype. Then the generalization of \(\tau\) with respect to \(\Gamma'\) is more general than the generalization of \(\tau\) with respect to \(\Gamma\).

theorem gen_moreGeneral {Γ' Γ : Ctx B} (h : Γ'.ftv ⊆ Γ.ftv) (τ : Ty B) :
    (gen Γ' τ).MoreGeneral (gen Γ τ)

Uses 13 · Used by 1

Statement usesTyping context · Free type variables of a context · More general type scheme · Monotypes · Generalization of a monotype

Proof usesType schemes · Evaluation of a type scheme · Instantiation of a type scheme · Monotypes as type schemes · Terms for unification · Applying a substitution to a term · Substitution depends only on the variables of the term · Variables of a term

Used byTyping is preserved in more general contexts

TheoremTyping is preserved in more general contexts#✓fully proved

If \(\Gamma \vdash e : \tau\) and \(\Gamma'\) is a context more general than \(\Gamma\), then \(\Gamma' \vdash e : \tau\).

theorem HasType.mono {Γ : Ctx B} {e : Expr} {τ : Ty B} (hτ : HasType Γ e τ) :
    ∀ {Γ' : Ctx B}, Γ'.MoreGeneral Γ → HasType Γ' e τ

Uses 17 · Used by 3

Statement usesTyping context · More general context · Expressions of the λ-calculus with let · Hindley–Milner typing · Monotypes

Proof usesExtending more general contexts by a binding · Free type variables of a context · Context lookup · Free type variables of a name's visible scheme · Type schemes · More general type scheme · Instantiation of a type scheme · Generalization of a monotype · Generalizing in a context with fewer free variables · Monotypes as type schemes · Terms for unification · Variables of a term

Used byThe let rule under a type substitution · Hindley–Milner typing is stable under type substitution · Completeness of Algorithm W

DefinitionStrict upper bound of a finite set of naturals#✓fully proved

For a finite set \(S\) of natural numbers, this is the number \(\max S + 1\), where the maximum of the empty set is taken to be \(0\). It is strictly greater than every element of \(S\).

def above (S : Finset ℕ) : ℕ := S.sup id + 1

Used by 4

Used byRenaming step of the substitution lemma · let generalizes · The let rule under a type substitution · Hindley–Milner typing is stable under type substitution

TheoremRenaming step of the substitution lemma#✓fully proved

Let \(\Gamma\) be a typing context, \(\tau\) a monotype and \(s\) a type substitution. Write \(s\Gamma\) for the context obtained by applying \(s\) to every scheme of \(\Gamma\), and let \(N\) be one more than the largest free type variable of \(s\Gamma\), with \(N = 1\) if \(s\Gamma\) has none. Let \(\rho\) be the substitution sending a type variable \(y\) to \(s(y)\) if \(y\) is free in \(\Gamma\), and to the type variable \(y + N\) otherwise. Then the generalization of \(\rho(\tau)\) with respect to \(s\Gamma\) is more general than the scheme obtained by applying \(s\) to the free type variables of the generalization of \(\tau\) with respect to \(\Gamma\).

theorem gen_subst_moreGeneral (Γ : Ctx B) (τ : Ty B) (s : Subst B) :
    (gen (Γ.subst s) (τ.subst fun y ↦
        if y ∈ Γ.ftv then s y else Term.var (y + above (Γ.subst s).ftv))).MoreGeneral
      ((gen Γ τ).substTy s)

Uses 21 · Used by 2

Statement usesTyping context · Free type variables of a context · Applying a type substitution to a context · More general type scheme · Applying a type substitution to a scheme · Monotypes · Strict upper bound of a finite set of naturals · Generalization of a monotype · Substitution · Terms for unification · Applying a substitution to a term

Proof usesContext lookup · Free type variables of a name's visible scheme · Type schemes · Evaluation of a type scheme · Instantiation of a type scheme · Monotypes as type schemes · Variables of a substituted term · Substitution depends only on the variables of the term · Variables of a term · Variables of a substituted variable occur in the substituted term

Used byThe let rule under a type substitution · Hindley–Milner typing is stable under type substitution

TheoremHindley–Milner typing is stable under type substitution#✓fully proved

Let \(\Gamma\) be a typing context, \(e\) an expression and \(\tau\) a monotype with \(\Gamma \vdash e : \tau\). Then for every type substitution \(s\), \(s\Gamma \vdash e : s\tau\), where \(s\Gamma\) applies \(s\) to every scheme of \(\Gamma\) and \(s\tau\) applies \(s\) to \(\tau\).

theorem HasType.subst {Γ : Ctx B} {e : Expr} {τ : Ty B} (hτ : HasType Γ e τ) :
    ∀ s : Subst B, HasType (Γ.subst s) e (τ.subst s)

Uses 23 · Used by 2

Statement usesTyping context · Applying a type substitution to a context · Expressions of the λ-calculus with let · Hindley–Milner typing · Monotypes · Substitution · Applying a substitution to a term

Proof usesMore general context · Extending more general contexts by a binding · Contexts with the same lookups are related by generality · Free type variables of a context · Context lookup · Substitutions agreeing on a context give the same lookups · Typing is preserved in more general contexts · Type schemes · Instantiation of a type scheme · Applying a type substitution to a scheme · Strict upper bound of a finite set of naturals · Generalization of a monotype · Renaming step of the substitution lemma · Instantiation commutes with substitution · Monotypes as type schemes · Terms for unification

Used bySoundness of Algorithm W · The let rule under a type substitution

TheoremTyping inversion for variables#✓fully proved

Let \(\Gamma\) be a typing context, \(x\) a name and \(\tau\) a monotype. Then \(\Gamma \vdash x : \tau\) holds for the variable expression \(x\) if and only if there are a type scheme \(\sigma\) and monotypes \((t_i)_{i \in \mathbb{N}}\) such that the lookup of \(x\) in \(\Gamma\) gives \(\sigma\) and \(\tau\) is the instance of \(\sigma\) at \((t_i)\).

theorem hasType_var_iff {Γ : Ctx B} {x : String} {τ : Ty B} :
    HasType Γ (.var x) τ ↔ ∃ σ ts, Γ.lookup x = some σ ∧ τ = σ.inst ts

Uses 10 · Used by 2

Statement usesTyping context · Context lookup · Expressions of the λ-calculus with let · Hindley–Milner typing · Type schemes · Instantiation of a type scheme · Monotypes

Proof usesGeneralization of a monotype · Monotypes as type schemes · Terms for unification

Used byThe abstraction \(\lambda f.\, f\, f\) has no type · Completeness of Algorithm W

TheoremNo monotype is an arrow out of itself#✓fully proved

For all monotypes \(\tau_1\) and \(\tau_2\), \(\tau_1 \ne (\tau_1 \to \tau_2)\).

theorem ne_node_self_left (τ₁ τ₂ : Ty B) : τ₁ ≠ node τ₁ τ₂

Uses 3 · Used by 1

Statement usesMonotypes · Terms for unification

Proof usesSize of a term

Used byThe abstraction \(\lambda f.\, f\, f\) has no type

TheoremThe abstraction \(\lambda f.\, f\, f\) has no type#✓fully proved

For every typing context \(\Gamma\), every variable name \(f\) and every monotype \(\tau\), the judgment \(\Gamma \vdash \lambda f.\, f\, f : \tau\) does not hold.

The λ-bound variable \(f\) is monomorphic, so it cannot be applied to itself.

theorem not_hasType_lam_self_app (Γ : Ctx B) (f : String) (τ : Ty B) :
    ¬ HasType Γ (.lam f (.app (.var f) (.var f))) τ

Uses 14

Statement usesTyping context · Expressions of the λ-calculus with let · Hindley–Milner typing · Monotypes

Proof usesContext lookup · Type schemes · Evaluation of a type scheme · Instantiation of a type scheme · Generalization of a monotype · Typing inversion for variables · No monotype is an arrow out of itself · Monotypes as type schemes · Terms for unification · Applying a substitution to a term

Theoremlet generalizes#✓fully proved

For every typing context \(\Gamma\), all variable names \(f\) and \(x\), and every type variable \(\alpha\), the expression \(\mathtt{let}\ f = \lambda x.\, x\ \mathtt{in}\ f\, f\) has type \(\alpha \to \alpha\) in \(\Gamma\).

theorem hasType_let_id_app_id (Γ : Ctx B) (f x : String) (α : ℕ) :
    HasType Γ (.let_ f (.lam x (.var x)) (.app (.var f) (.var f)))
      (node (Term.var α) (Term.var α))

Uses 14

Statement usesTyping context · Expressions of the λ-calculus with let · Hindley–Milner typing · Terms for unification

Proof usesFree type variables of a context · Context lookup · Type schemes · Evaluation of a type scheme · Instantiation of a type scheme · Monotypes · Strict upper bound of a finite set of naturals · Generalization of a monotype · Monotypes as type schemes · Applying a substitution to a term

TheoremThe let rule under a type substitution#✓fully proved

Let \(\Gamma\) be a typing context, \(s\) a type substitution, \(x\) a variable name, \(e_1, e_2\) expressions and \(\tau_1, \tau_2\) monotypes, and write \(s\Gamma\) for the context obtained by applying \(s\) to every type scheme of \(\Gamma\). Suppose \(e_1\) has type \(\tau_1\) in \(\Gamma\), and \(e_2\) has type \(\tau_2\) in the context obtained from \(s\Gamma\) by binding \(x\), in front, to the type scheme that results from applying \(s\) to the generalization of \(\tau_1\) in \(\Gamma\). Then \(\mathtt{let}\ x = e_1\ \mathtt{in}\ e_2\) has type \(\tau_2\) in \(s\Gamma\).

theorem HasType.let_substTy {Γ : Ctx B} {x : String} {e₁ e₂ : Expr} {τ₁ τ₂ : Ty B}
    (s : Subst B) (h₁ : HasType Γ e₁ τ₁)
    (h₂ : HasType ((x, (gen Γ τ₁).substTy s) :: Γ.subst s) e₂ τ₂) :
    HasType (Γ.subst s) (.let_ x e₁ e₂) τ₂

Uses 21 · Used by 1

Statement usesTyping context · Applying a type substitution to a context · Expressions of the λ-calculus with let · Hindley–Milner typing · Type schemes · Applying a type substitution to a scheme · Monotypes · Generalization of a monotype · Substitution

Proof usesMore general context · Extending more general contexts by a binding · Contexts with the same lookups are related by generality · Free type variables of a context · Context lookup · Substitutions agreeing on a context give the same lookups · Typing is preserved in more general contexts · Hindley–Milner typing is stable under type substitution · Strict upper bound of a finite set of naturals · Renaming step of the substitution lemma · Terms for unification · Applying a substitution to a term

Used bySoundness of Algorithm W

DefinitionBound-variable supremum of a type scheme#✓fully proved

The bound-variable supremum of a type scheme \(\sigma\) is one more than the largest index \(i\) of a bound variable occurring in \(\sigma\), and \(0\) if no bound variable occurs in \(\sigma\).

def Scheme.boundSup : Scheme B → ℕ
  | Term.var _ => 0
  | Term.const (Sum.inl _) => 0
  | Term.const (Sum.inr i) => i + 1
  | Term.node l r => max (Scheme.boundSup l) (Scheme.boundSup r)

Uses 2 · Used by 4

Statement usesType schemes · Terms for unification

Used bySoundness of Algorithm W · Algorithm W · Completeness of Algorithm W · Freshness invariants of Algorithm W

DefinitionAlgorithm W#✓fully proved

Given a typing context \(\Gamma\), an expression \(e\) and a counter \(n\), Algorithm W either fails or returns a substitution, a monotype and a new counter; type variables \(\alpha_m\) with \(m \ge n\) serve as fresh. Write \(\tau_1 \to \tau_2\) for the arrow type, \(s\Gamma\) for \(\Gamma\) with the substitution \(s\) applied to every type scheme, and \(s(\tau)\) for \(s\) applied to a monotype \(\tau\). Algorithm W is defined by recursion on \(e\), and fails as soon as a recursive call or a unification fails:

• For a variable \(x\): if \(x\) is unbound in \(\Gamma\), W fails; otherwise, with \(\sigma\) the visible type scheme of \(x\), W returns the identity substitution, the instance of \(\sigma\) that replaces each bound variable \(i\) by \(\alpha_{n+i}\), and the counter \(n + k\), where \(k\) is one more than the largest bound-variable index of \(\sigma\) (\(0\) if it has none).
• For \(\lambda x.\, e'\): W runs on the context \(\Gamma\) with \(x\) bound in front to the monotype \(\alpha_n\), the body \(e'\) and the counter \(n + 1\); if this returns \((s, \tau, n')\), W returns \((s, s(\alpha_n) \to \tau, n')\).
• For an application \(e_1\, e_2\): W runs on \(\Gamma\), \(e_1\), \(n\), giving \((s_1, \tau_1, n_1)\), then on \(s_1\Gamma\), \(e_2\), \(n_1\), giving \((s_2, \tau_2, n_2)\), then runs unification on the single equation \(s_2(\tau_1) = \tau_2 \to \alpha_{n_2}\), giving \(s_3\); it returns the composite substitution applying \(s_1\), then \(s_2\), then \(s_3\), the type \(s_3(\alpha_{n_2})\) and the counter \(n_2 + 1\).
• For \(\mathtt{let}\ x = e_1\ \mathtt{in}\ e_2\): W runs on \(\Gamma\), \(e_1\), \(n\), giving \((s_1, \tau_1, n_1)\), then on the context \(s_1\Gamma\) with \(x\) bound in front to the generalization of \(\tau_1\) in \(s_1\Gamma\), \(e_2\) and \(n_1\), giving \((s_2, \tau_2, n_2)\); it returns the composite substitution applying \(s_1\) then \(s_2\), the type \(\tau_2\) and the counter \(n_2\).

Cslib.HindleyMilner.W · 16 lines

def W (Γ : Ctx B) : Expr → ℕ → Option (Subst B × Ty B × ℕ)
  | .var x, n =>
    (Γ.lookup x).map fun σ ↦ (Term.var, σ.inst (fun i ↦ Term.var (n + i)), n + σ.boundSup)
  | .lam x e, n =>
    (W ((x, toScheme (Term.var n)) :: Γ) e (n + 1)).map fun (s, τ, n') ↦
      (s, node ((Term.var n).subst s) τ, n')
  | .app e₁ e₂, n => do
    let (s₁, τ₁, n₁) ← W Γ e₁ n
    let (s₂, τ₂, n₂) ← W (Γ.subst s₁) e₂ n₁
    let s₃ ← unify [(τ₁.subst s₂, node τ₂ (Term.var n₂))]
    return (s₁ ≫ s₂ ≫ s₃, (Term.var n₂).subst s₃, n₂ + 1)
  | .let_ x e₁ e₂, n => do
    let (s₁, τ₁, n₁) ← W Γ e₁ n
    let (s₂, τ₂, n₂) ← W ((x, gen (Γ.subst s₁) τ₁) :: Γ.subst s₁) e₂ n₁
    return (s₁ ≫ s₂, τ₂, n₂)
termination_by e => sizeOf e

Uses 15 · Used by 6

Statement usesTyping context · Context lookup · Applying a type substitution to a context · Expressions of the λ-calculus with let · Type schemes · Bound-variable supremum of a type scheme · Instantiation of a type scheme · Monotypes · Generalization of a monotype · Monotypes as type schemes · Substitution · Composition of substitutions on first-order terms · Terms for unification · Applying a substitution to a term · Martelli–Montanari unification

Used bySoundness of type inference for closed expressions · Soundness of Algorithm W · Type inference for closed expressions · Completeness of type inference for closed expressions · Completeness of Algorithm W · Freshness invariants of Algorithm W

DefinitionType inference for closed expressions#✓fully proved

Type inference on an expression \(e\) runs Algorithm W on \(e\) in the empty context with fresh-variable counter \(0\). If W succeeds with a substitution \(s\), a monotype \(\tau\) and a counter \(n'\), the inferred type of \(e\) is \(\tau\); if W fails, \(e\) has no inferred type.

def infer (e : Expr) : Option (Ty B) := (W [] e 0).map fun r ↦ r.2.1

Uses 5 · Used by 4

Statement usesExpressions of the λ-calculus with let · Type schemes · Monotypes · Algorithm W · Substitution

Used bySoundness of type inference for closed expressions · Completeness of type inference for closed expressions · Type inference succeeds exactly on typable closed expressions · Principal types

TheoremSoundness of Algorithm W#✓fully proved

Let \(\Gamma\) be a typing context, \(e\) an expression and \(n\) a natural number. If Algorithm W, run on \(\Gamma\) and \(e\) with fresh-variable counter \(n\), succeeds and returns a substitution \(s\), a monotype \(\tau\) and a counter \(n'\), then \(e\) has type \(\tau\) in the context \(s\Gamma\) obtained by applying \(s\) to every type scheme of \(\Gamma\).

theorem hasType_of_W_eq_some {e : Expr} :
    ∀ {Γ : Ctx B} {n : ℕ} {s : Subst B} {τ : Ty B} {n' : ℕ},
      W Γ e n = some (s, τ, n') → HasType (Γ.subst s) e τ

Uses 23 · Used by 1

Statement usesTyping context · Applying a type substitution to a context · Expressions of the λ-calculus with let · Hindley–Milner typing · Monotypes · Algorithm W · Substitution

Proof usesContext lookup · The let rule under a type substitution · Hindley–Milner typing is stable under type substitution · Type schemes · Bound-variable supremum of a type scheme · Instantiation of a type scheme · Applying a type substitution to a scheme · Generalization of a monotype · Monotypes as type schemes · Lists of equations · Composition of substitutions on first-order terms · Terms for unification · Applying a substitution to a term · Unifier of a list of equations · Soundness of unification · Martelli–Montanari unification

Used bySoundness of type inference for closed expressions

TheoremSoundness of type inference for closed expressions#✓fully proved

For every expression \(e\) and monotype \(\tau\), if type inference for closed expressions returns \(\tau\) on \(e\), then \(e\) has type \(\tau\) in the empty context.

theorem hasType_of_infer_eq_some {e : Expr} {τ : Ty B} (h : infer e = some τ) :
    HasType [] e τ

Uses 11 · Used by 2

Statement usesExpressions of the λ-calculus with let · Hindley–Milner typing · Type schemes · Monotypes · Type inference for closed expressions

Proof usesTyping context · Applying a type substitution to a context · Applying a type substitution to a scheme · Algorithm W · Soundness of Algorithm W · Substitution

Used byType inference succeeds exactly on typable closed expressions · Principal types

DefinitionVariables below a bound#✓fully proved

A term \(t\) has all its variables below \(n\) when every variable \(z\) occurring in \(t\) satisfies \(z < n\).

def VarsBelow (n : ℕ) (t : Term B) : Prop := ∀ z ∈ t.vars, z < n

Uses 2 · Used by 2

Statement usesTerms for unification · Variables of a term

Used byCompleteness of Algorithm W · Freshness invariants of Algorithm W

TheoremFreshness invariants of Algorithm W#✓fully proved

Let \(\Gamma\) be a typing context and \(n\) a natural number such that every free type variable of \(\Gamma\) is less than \(n\). If Algorithm W succeeds on \(\Gamma\) and an expression \(e\) with counter \(n\), returning a substitution \(s\), a monotype \(\tau\) and a new counter \(n'\), then \(n \le n'\), every type variable of \(\tau\) is less than \(n'\), and for every type variable \(x < n\) every type variable of \(s(x)\) is less than \(n'\).

theorem W_fresh {e : Expr} :
    ∀ {Γ : Ctx B} {n : ℕ} {s : Subst B} {τ : Ty B} {n' : ℕ}, (∀ z ∈ Γ.ftv, z < n) →
      W Γ e n = some (s, τ, n') →
      n ≤ n' ∧ VarsBelow n' τ ∧ ∀ x < n, VarsBelow n' (s x)

Uses 25 · Used by 1

Statement usesTyping context · Free type variables of a context · Expressions of the λ-calculus with let · Monotypes · Variables below a bound · Algorithm W · Substitution

Proof usesContext lookup · Applying a type substitution to a context · Free type variables of a name's visible scheme · Type schemes · Bound-variable supremum of a type scheme · Evaluation of a type scheme · Instantiation of a type scheme · Applying a type substitution to a scheme · Generalization of a monotype · Monotypes as type schemes · Composition of substitutions on first-order terms · Terms for unification · Variables of a substituted term · Applying a substitution to a term · Variables of a term · Variables of a list of equations · Martelli–Montanari unification · Unification introduces no new variables

Used byCompleteness of Algorithm W

TheoremSubstituting into a generalization is more general#✓fully proved

For a typing context \(\Gamma\), a monotype \(\tau\) and a type substitution \(r\), the scheme obtained by applying \(r\) to the free type variables of the generalization of \(\tau\) in \(\Gamma\) is more general than the generalization of \(r(\tau)\) in \(r(\Gamma)\): every instance of the latter is an instance of the former, and every free type variable of the former is a free type variable of the latter.

theorem substTy_gen_moreGeneral (Γ : Ctx B) (τ : Ty B) (r : Subst B) :
    ((gen Γ τ).substTy r).MoreGeneral (gen (Γ.subst r) (τ.subst r))

Uses 20 · Used by 1

Statement usesTyping context · Applying a type substitution to a context · More general type scheme · Applying a type substitution to a scheme · Monotypes · Generalization of a monotype · Substitution · Applying a substitution to a term

Proof usesFree type variables of a context · Context lookup · Free type variables of a name's visible scheme · Type schemes · Evaluation of a type scheme · Instantiation of a type scheme · Monotypes as type schemes · Terms for unification · Variables of a substituted term · Substitution depends only on the variables of the term · Variables of a term · Variables of a substituted variable occur in the substituted term

Used byCompleteness of Algorithm W

TheoremGeneralization depends only on the free variables of the context#✓fully proved

If two typing contexts \(\Gamma\) and \(\Gamma'\) have the same free type variables, then for every monotype \(\tau\) the generalization of \(\tau\) in \(\Gamma\) equals the generalization of \(\tau\) in \(\Gamma'\).

theorem gen_congr {Γ Γ' : Ctx B} (h : Γ.ftv = Γ'.ftv) (τ : Ty B) : gen Γ τ = gen Γ' τ

Uses 8 · Used by 1

Statement usesTyping context · Free type variables of a context · Type schemes · Monotypes · Generalization of a monotype

Proof usesMonotypes as type schemes · Terms for unification · Applying a substitution to a term

Used byCompleteness of Algorithm W

TheoremCompleteness of Algorithm W#✓fully proved

Let \(\Gamma\) be a typing context and \(n\) a natural number such that every free type variable of \(\Gamma\) is less than \(n\). If, for some type substitution \(u\), an expression \(e\) has a monotype \(\tau'\) in the context \(u(\Gamma)\), then Algorithm W succeeds on \(\Gamma\) and \(e\) with counter \(n\), returning a substitution \(s\), a monotype \(\tau\) and a new counter \(n'\), and there is a type substitution \(r\) such that \(u(x) = r(s(x))\) for every type variable \(x < n\), and \(\tau' = r(\tau)\).

This is the completeness theorem of Damas and Milner.

theorem W_complete {e : Expr} :
    ∀ {Γ : Ctx B} {n : ℕ} {u : Subst B} {τ' : Ty B}, (∀ z ∈ Γ.ftv, z < n) →
      HasType (Γ.subst u) e τ' →
      ∃ s τ n' r, W Γ e n = some (s, τ, n') ∧ (∀ x < n, u x = (s x).subst r) ∧
        τ' = τ.subst r

Uses 39 · Used by 1

Statement usesTyping context · Free type variables of a context · Applying a type substitution to a context · Expressions of the λ-calculus with let · Hindley–Milner typing · Monotypes · Algorithm W · Substitution · Terms for unification · Applying a substitution to a term

Proof usesExtending more general contexts by a binding · Contexts with the same lookups are related by generality · Free type variables depend only on visible bindings · Context lookup · Substitutions agreeing on a context give the same lookups · Free type variables of a name's visible scheme · Typing is preserved in more general contexts · Type schemes · More general type scheme · Bound-variable supremum of a type scheme · Evaluation of a type scheme · Instantiation of a type scheme · Applying a type substitution to a scheme · Variables below a bound · Freshness invariants of Algorithm W · Generalization of a monotype · Generalization depends only on the free variables of the context · Typing inversion for variables · Substituting into a generalization is more general · Monotypes as type schemes · Lists of equations · Composition of substitutions on first-order terms · Variables of a substituted term · Substitution depends only on the variables of the term · Variables of a term · Unifier of a list of equations · Martelli–Montanari unification · Completeness of unification · Most generality of unification

Used byCompleteness of type inference for closed expressions

TheoremCompleteness of type inference for closed expressions#✓fully proved

If an expression \(e\) has a monotype \(\tau'\) in the empty context, then type inference succeeds on \(e\) and returns a monotype \(\tau\) of which \(\tau'\) is a substitution instance: \(\tau' = r(\tau)\) for some type substitution \(r\).

theorem infer_complete {e : Expr} {τ' : Ty B} (h : HasType [] e τ') :
    ∃ τ, infer e = some τ ∧ ∃ r, τ' = τ.subst r

Uses 15 · Used by 2

Statement usesExpressions of the λ-calculus with let · Hindley–Milner typing · Type schemes · Monotypes · Type inference for closed expressions · Substitution · Applying a substitution to a term

Proof usesTyping context · Free type variables of a context · Applying a type substitution to a context · Free type variables of a name's visible scheme · Applying a type substitution to a scheme · Algorithm W · Completeness of Algorithm W · Terms for unification

Used byType inference succeeds exactly on typable closed expressions · Principal types

TheoremType inference succeeds exactly on typable closed expressions#✓fully proved

Type inference succeeds on an expression \(e\) if and only if \(e\) has some monotype in the empty context.

theorem infer_isSome_iff {e : Expr} :
    (infer (B := B) e).isSome ↔ ∃ τ : Ty B, HasType ([] : Ctx B) e τ

Uses 9

Statement usesExpressions of the λ-calculus with let · Hindley–Milner typing · Type schemes · Monotypes · Type inference for closed expressions

Proof usesSoundness of type inference for closed expressions · Completeness of type inference for closed expressions · Substitution · Applying a substitution to a term

TheoremPrincipal types#✓fully proved

The inferred type of a closed expression is one of its types, and every type of it is an instance of the inferred one.

theorem infer_principal {e : Expr} {τ : Ty B} (h : infer e = some τ) :
    HasType [] e τ ∧ ∀ τ', HasType [] e τ' → ∃ r, τ' = τ.subst r

Uses 9

Statement usesExpressions of the λ-calculus with let · Hindley–Milner typing · Type schemes · Monotypes · Type inference for closed expressions · Substitution · Applying a substitution to a term

Proof usesSoundness of type inference for closed expressions · Completeness of type inference for closed expressions

45 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.