Skip to main content

​
Type Inference Algorithm

Elara implements a complete Hindley-Milner type inference system with support for let-polymorphism, higher-kinded types, and limited higher-rank types. The type inference engine automatically deduces types for all expressions without requiring explicit type annotations.

​
Overview

The type inference system follows the classic constraint-based approach:
1

Constraint Generation

Walk the AST and generate type equality constraints
2

Constraint Solving

Unify types to find a substitution that satisfies all constraints
3

Generalization

Abstract over unbound type variables to create polytypes
4

Instantiation

Replace quantified type variables with fresh unification variables

​
Type System Foundations

​
Monotypes and Polytypes

Elara distinguishes between two kinds of types:
  • Monotypes (τ): Simple, non-polymorphic types
    • Type variables: α, β
    • Type constructors: Int, String, Bool
    • Function types: τ₁ → τ₂
    • Applications: List α, Option Int
  • Polytypes (σ): Polymorphic types with universal quantification
    • ∀α. α → α (identity function)
    • ∀α β. (α → β) → List α → List β (map function)
Let-Polymorphism: Only let-bound variables can have polytypes. Lambda parameters are always monomorphic (this is a key difference from System F).

​
Type Variables

The inference engine uses two kinds of type variables: 
data TypeVariable 
  = UnificationVar UniqueTyVar  -- Can be substituted during unification
  | SkolemVar UniqueTyVar       -- Rigid variables from type signatures
Unification variables (α₁, α₂, ...) are generated fresh during inference and represent unknown types. Skolem variables are introduced when checking against user-provided type signatures and must not be unified with other types.

​
Constraint Generation

The constraint generation phase traverses the Shunted AST and generates type equality constraints.

​
Core Rules

(x : ∀α. Q ⇒ τ) ∈ Γ
─────────────────────
Γ ⊢ x : [α ↦ β]τ ⊣ [α ↦ β]Q
Lookup the variable’s type in the environment, instantiate it with fresh type variables, and emit the instantiated constraints.
Γ, x:α ⊢ e : τ
──────────────────
Γ ⊢ λx.e : α → τ
Generate a fresh type variable α for the parameter, extend the environment, and infer the body type τ.
Γ ⊢ e₁ : τ₁    Γ ⊢ e₂ : τ₂    β fresh
────────────────────────────────────────
Γ ⊢ e₁ e₂ : β ⊣ (τ₁ ∼ τ₂ → β)
Infer both subexpressions, generate a fresh result type β, and emit constraint τ₁ ∼ τ₂ → β.
Γ ⊢ e₁ : τ₁    Γ, x:gen(τ₁) ⊢ e₂ : τ₂
────────────────────────────────────────
Γ ⊢ let x = e₁ in e₂ : τ₂
Infer the bound expression, generalize its type (abstract over free type variables), and use the polytype when inferring the body.
Elara detects recursive bindings and avoids generalization to prevent unsound types.
Γ ⊢ e : τ    ∀i. Γ ⊢ pᵢ : τ  Γ, vars(pᵢ) ⊢ eᵢ : τᵣ
─────────────────────────────────────────────────────
Γ ⊢ match e with {p₁ → e₁; ...; pₙ → eₙ} : τᵣ
All patterns must match the scrutinee type τ, and all branches must return the same result type τᵣ.

​
Constructor Patterns

When type-checking constructor patterns, the system:
  1. Looks up the constructor’s signature (e.g., Some : ∀α. α → Option α)
  2. Instantiates the polytype with fresh unification variables
  3. Matches the constructor’s argument types against the pattern arguments
  4. Emits equality constraints
type Option a = Some a | None

match value with
  Some x -> x  // x : α where value : Option α
  None -> defaultValue

​
Constraint Solving (Unification)

The solver processes constraints to find a substitution S that makes all equalities hold.

​
Unification Algorithm

The unification algorithm unify(τ₁, τ₂) is defined recursively: 
unify(α, α) = {}
Nothing to do.
unify(α, τ) = [α ↦ τ]  if α ∉ ftv(τ)
            = fail      otherwise (occurs check)
Bind the variable to the type, unless the variable appears in the type (which would create an infinite type).
unify(C τ₁...τₙ, C σ₁...σₘ) = 
  if n ≠ m then fail (arity mismatch)
  else compose(unify(τ₁, σ₁), ..., unify(τₙ, σₙ))

unify(C ..., D ...) where C ≠ D = 
  try expanding type aliases, else fail
Recursively unify corresponding arguments. Different constructors fail unless one is a type alias.
unify(α → β, γ → δ) = compose(unify(α, γ), unify(β, δ))
Function types unify structurally.

​
Type Alias Expansion

When unification fails between type constructors, the system attempts to expand type aliases: 
type alias Name = String

// Unifying 'Name' with 'String' succeeds by expanding the alias
let greet : String -> String
let greet (n : Name) = "Hello, " <> n
Recursive type aliases are supported and essential for expressing types like:
type Person = { name: String, friends: [Person] }

​
Generalization

Generalization converts a monotype to a polytype by quantifying over free type variables: 
gen(τ, Γ) = ∀(ftv(τ) \ ftv(Γ)). τ
Only variables not free in the environment are generalized. This prevents: 
let f = λx → 
  let g = λy → x  // DON'T generalize x here!
  in (g 1, g "hello")  // Would be unsound

​
Value Restriction

Elara implements the value restriction: only syntactic values (lambdas, constructors) can be generalized. This prevents issues with side effects: 
let r = ref None  // Not a value! Don't generalize.
let x = get r     // Uses monomorphic type

​
Instantiation

Instantiation replaces quantified variables with fresh unification variables: 
inst(∀α₁...αₙ. Q ⇒ τ) = [α₁ ↦ β₁, ..., αₙ ↦ βₙ]τ, [α₁ ↦ β₁, ..., αₙ ↦ βₙ]Q
where β₁, ..., βₙ are fresh.

​
Error Reporting

The type checker provides detailed error messages with context: 
Error: Type mismatch
  Expected: Int
  Found:    String
  In:       argument 1 of function 'add'
  Location: example.elara:5:12

Error: Cannot construct infinite type
  α ~ List α
  When checking: recursive list definition

Error: Constructor 'Some' expects 1 argument
  Found: 2 arguments
  In pattern: Some x y

​
Implementation Details

​
Source Location

The implementation at src/Elara/TypeInfer/ConstraintGeneration.hs includes:
  • Constraint generation: generateConstraints :: ShuntedExpr -> Eff (TypedExpr, Monotype)
  • Unification: unify :: Monotype -> Monotype -> Eff (Constraint, Substitution)
  • Solver: solveConstraint :: Constraint -> Set UniqueTyVar -> Constraint -> Eff (Constraint, Substitution)

​
Optimization

The type inference engine achieves > 300% performance improvement through:
  1. Efficient union-find for type variable representatives
  2. Memoization of constraint solving results
  3. Lazy constraint generation (integrated with Rock query system)

​
Further Reading

Build docs developers (and LLMs) love

Get started for freeTalk to us