Implement Type Inference for a Simple Expression Language

Topic Overview

Inferring Types Without Annotations

ML, Haskell, Rust, and TypeScript infer types where annotations are omitted. Hindley-Milner unification assigns types to every subexpression; Rust's solver handles traits. Even a simple constraint-based inferencer for arithmetic expressions teaches the core idea.

Unification on Expressions

Literals get concrete types: 42 is int, 3.14 is float. For a + b, unify a and b to the same numeric type; result matches. For if c then e1 else e2, unify e1 and e2; c must be bool.

cCopy
Loading…

• Generate type variables for unknown identifiers
• Constraints: add : int -> int -> int or polymorphic
• Solve by unification or fixed-point iteration
• Report ambiguous or unsolvable constraints as errors

Connecting to real compilers

Production compilers embed this step inside a longer pipeline. GCC flows through cpp, cc1, assembly, and ld; Clang uses the driver, Sema, LLVM IR passes, and a target backend. LLVM bitcode, JVM bytecode, and WASM are other familiar IRs at the same layer. The exercise isolates one pass so you can test it alone before chaining it to the next stage.

Why for this exercise

You will implement type inference for a small expression language without explicit type annotations. This exercise requires generating constraints from the AST and solving them to assign types to every subexpression.

Your Task

Implement Hindley (Milner type inference (Algorithm W, or its destructive-unification variant) for a tiny functional language: no type annotations anywhere, yet every expression gets its most general type) including polymorphic ones like 'a -> 'a.

The language

One expression per line (blank lines ignored):

cCopy
Loading…

Identifiers are [A-Za-z_][A-Za-z0-9_']* other than the keywords fun let in if then else true false.

Typing rules

• Literals: int, bool, string. + - * need int operands and give int; ^ needs and gives string; == unifies both sides and gives bool.
• if: condition unifies with bool, both branches unify with each other.
• Application f a: unify f's type with type(a) -> fresh.
• fun x -> e: x gets a fresh type variable, not generalised (lambda-bound variables are monomorphic).
• let x = e1 in e2: infer e1, then generalise every type variable that is not shared with the enclosing environment, so each use of x in e2 gets fresh copies. That's what lets let id = fun x -> x in id 1 == id 2 type-check.
• Unification includes the occurs check.

Output

INPUT : TYPE, where the type is printed with arrows right-associative (parenthesise an arrow on the left of another arrow) and type variables named 'a, 'b, 'c, … in order of first appearance reading the printed type left to right.

Errors replace the type (each test expression contains at most one error):

Example

Input:

cCopy
Loading…

Output:

cCopy
Loading…

Requirements

1. Type variables that can be bound (a union-find link or a substitution), unify with an occurs check, and instantiate / generalise for let-polymorphism.
2. Rename variables only when printing.

Hidden tests cover higher-order functions, currying and partial application, let-polymorphism vs lambda monomorphism, unbound variables, applying a non-function, and syntax errors.