Sketch of type inference without unification variables

typing.md

The inference judgment is:

Γ ⊢ e ⇒ A ⊢ Δ

… where:

• Γ (an input) is a context which is a map from variables to their types
• e (an input) is an expression whose type we wish to infer
• A (an output) is the inferred type
• Δ (an output) is a context which is a map from variables to their types

The checking judgment is:

Γ ⊢ e ⇐ A ⊢ Δ

… where:

• Γ (an input) is a context which is a map from variables to their types
• e (an input) is an expression whose type we wish to check
• A (an input) is the type to check against
• Δ (an output) is a context which is a map from variables to their types

The typing rules are:

──────────────────── Var ⇒
Γ, x : A ⊢ x ⇒ A ⊢ ·

───────────────── Var ⇐
Γ ⊢ x ⇐ A ⊢ x : A

Γ ⊢ e ⇒ B ⊢ Δ, x : A
──────────────────── Lam ⇒
Γ ⊢ λx.e ⇒ A → B ⊢ Δ

Γ, x : A ⊢ e ⇐ B ⊢ Δ
──────────────────── Lam ⇐
Γ ⊢ λx.e ⇐ A → B ⊢ Δ

Γ, x : A ⊢ e ⇒ B ⊢ Δ
────────────────────────── Lam + Annot ⇒
Γ ⊢ λ(x : A).e ⇒ A → B ⊢ Δ

Γ ⊢ f ⇒ A → B ⊢ Δ₀
Γ ⊢ x ⇐ A ⊢ Δ₁
Δ₀ ∩ Δ₁ = ∅
──────────────────── App ⇒
Γ ⊢ f x ⇒ B ⊢ Δ₀, Δ₁

Γ ⊢ x ⇒ A ⊢ Δ₀
Γ ⊢ f ⇐ A → B ⊢ Δ₁
Δ₀ ∩ Δ₁ = ∅
──────────────────── App ⇐
Γ ⊢ f x ⇐ B ⊢ Δ₀, Δ₁

Γ ⊢ e ⇐ A ⊢ Δ
───────────────── Annot ⇒
Γ ⊢ e : A ⇒ A ⊢ Δ