Instantly share code, notes, and snippets.

# Gabriella439/typing.md

Last active February 4, 2023 21:15
Show Gist options
• Save Gabriella439/72667551f5b4454b0f30403be6083b67 to your computer and use it in GitHub Desktop.
Sketch of type inference without unification variables

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 ⊢ Δ
``````