Hindley-Milner type inference

Algorithm W infers a type for every expression without type annotations. The part that makes it a good showcase for Elpi is that it turns some inferred types into schemes, universally quantified over the type variables used only locally: let id = λx.x in (id one, id empty) has to accept id at two different types. What follows walks through the core of it. The HDR thesis, §2.7, works through the same example in much more detail, subsection by subsection: syntax, typing rules, generalization, a full execution trace, and bidirectional type inference.

../code/hindley-milner.elpi:

% Algorithm W, with let-generalization deferred through a constraint: a type
% scheme is only generalized once we know everything that was unified into
% it, which happens after type-checking the let-bound expression, not before.
% Adapted from tests/sources/w.elpi.

% terms
data term.
symb app term -> term -> term.
symb lam (term -> term) -> term.
symb let term -> ty -> (term -> term) -> term.

% monotypes: type constructors applied to arguments (#) and the arrow (===>)
% (===> and # are recognised as infix automatically, by token family)
data tye.
symb (===>) tye -> tye -> tye.
symb (#)    tye -> tye -> tye.

% type schemes: mono wraps a monotype, all quantifies a type variable
data ty.
symb all  (tye -> ty) -> ty.
symb mono tye -> ty.

% a handful of constants and their (possibly polymorphic) schemes
symb one, plus, size, empty, comma  term.
symb integer, list, pair            tye.

% `w` stays relational: its last rule turns a type *scheme* into an instance
% by dispatching on whether the (output) type came back as `mono` or `all`,
% which the determinacy checker cannot follow through an output argument.
% In practice every top-level call has a single, principal type.
pred w term -> ty.
w one    (mono integer).
w plus   (mono (integer ===> integer ===> integer)).
w size   (all x\ mono (list # x ===> integer)).
w empty  (all x\ mono (list # x)).
w comma  (all x\ all y\ mono (x ===> y ===> (pair # x # y))).

w (app F X) (mono R) :-
  w F (mono (A ===> R)),
  w X (mono A).

w (lam F) (mono (A ===> R)) :-
  pi x\ w x (mono A) ==> w (F x) (mono R).

w (let F FP B) (mono TC) :-
  w F (mono FT),
  % FP is generalized only once, by the CHR rule below, after this branch
  % of the search is done computing constraints on FT
  declare_constraint (overbar (mono FT) FP) [],
  pi x\ w x FP ==> w (B x) (mono TC).

w X (mono T) :- w X (all Poly), specialize (all Poly) T.

func specialize ty -> tye.
specialize (all F) T :- specialize (F FRESH_) T.
specialize (mono X) X.

% overbar generalizes a monotype into a type scheme, once its context Gamma
% (the hypothetical `w` rules in scope) is fully known. `w ?-` is the context
% filter: it keeps those `w` rules in the context a suspended `overbar`
% constraint carries, so the rule below can see Gamma as `G`.
func overbar ty -> ty.
constraint w ?- overbar {
  rule \ (G ?- overbar T T1)
       | (generalize G T POLYT) <=> (T1 = POLYT).
}

func generalize list (pred), ty -> ty.
generalize G (mono T) ALL :-
  free-ty (mono T) [] VT,
  free-gamma G [] VG,
  filter VT (x\ not (mem VG x)) Q,
  quantify Q T ALL.

func free-ty ty, list any -> list any.
free-ty (mono X) L L1 :- free X L L1.
free-ty (all F) L L1 :- pi x\ free-ty (F x) L L1.

func free-gamma list (pred), list any -> list any.
free-gamma [] L L.
free-gamma [w _ T|X] L L2 :- free-ty T L L1, free-gamma X L1 L2.

func free tye, list any -> list any.
free (A # B) L L2 :- free A L L1, free B L1 L2.
free (A ===> B) L L2 :- free A L L1, free B L1 L2.
free (uvar X _) L L1 :- if (mem L X) (L1 = L) (L1 = [X|L]).

func copy-ty ty -> ty.
copy-ty (mono X1) (mono X2) :- copy X1 X2.
copy-ty (all F1) (all F2) :- pi x\ copy x x =!=> copy-ty (F1 x) (F2 x).

func copy tye -> tye.
copy (A ===> B) (A1 ===> B1) :- copy A A1, copy B B1.
copy (A # B) (A1 # B1) :- copy A A1, copy B B1.
copy (uvar _ _ as X) X.

func quantify list tye, tye -> ty.
quantify [] X (mono X1) :- copy X X1.
quantify [X|XS] T (all x\ T2 x) :-
  quantify XS T T1,
  pi x\ copy (uvar X _) x =!=> copy-ty T1 (T2 x).

% generic list helpers
func filter list A, (pred A) -> list A.
filter [] _ [].
filter [X|XS] P [X|YS] :- P X, !, filter XS P YS.
filter [_|XS] P YS :- filter XS P YS.

func mem list A, A.
mem [X|_] X :- !.
mem [_|XS] X :- mem XS X.

main :-
  % let id = \x.x in plus (id one) (size (id empty))
  % `id` is generalized to a type scheme and used at two different types
  P = let (lam x\ x) IdTy (id\ app (app plus (app id one))
                                  (app size (app id empty))),
  w P TP, print "well typed, of type" TP,
  print "id generalized to" IdTy.

well typed, of type mono integer
id generalized to all c0 \ mono (c0 ===> c0)

IdTy, the type scheme inferred for id, prints as all c0 \ mono (c0 ===> c0), universally quantified over the one type variable used only locally, the scheme that then lets id be applied to both an integer and a list # integer in the same body.

A monotype is a type with no quantifiers: an arrow ===>, an applied type constructor # (as in list # integer), or a type variable, itself an ordinary Elpi unification variable, an existential hole (Constraints). A scheme is mono T (no quantification) or all F, universally quantifying one more variable and continuing as F applied to it. specialize goes the other way: given a scheme, it produces one monotype by picking a fresh unification variable for every all, the same mechanism pi uses for a fresh bound name, here applied to open a scheme’s quantifiers into fresh holes to be filled in by whatever unifies with them at this particular use.

The interesting rule is let:

w (let F FP B) (mono TC) :-
  w F (mono FT),
  declare_constraint (overbar (mono FT) FP) [],
  pi x\ w x FP ==> w (B x) (mono TC).

FP, the scheme eventually given to the let-bound name, is not computed on the spot. Generalizing FT means comparing its free type variables against the free type variables of Γ, the set of hypothetical w rules currently in scope: the ==> rules nested pi/let``s have added so far. Γ is not a first-class value an ordinary goal can inspect, which is beyond what ``pi/==> alone can do (Logic Programming). A constraint handling rule can: its sequent pattern (G ?- goal) binds G to the very context a suspended goal carries with it (Constraint handling rules, The constraint store). So generalization is written as a suspended overbar constraint, resolved by one CHR rule once the goal it is attached to is later matched:

constraint w ?- overbar {
  rule \ (G ?- overbar T T1)
       | (generalize G T POLYT) <=> (T1 = POLYT).
}

The w ?- before the clique is the context filter: without it, G would keep only overbar’s own (empty) set of clique rules; naming w there keeps the hypothetical w rules, Γ, in the context the suspended overbar constraint carries, which is what generalize reads.

generalize collects the free variables of the monotype and of Γ, and quantifies those that are free in the former but not the latter, the ones the surrounding context makes no assumption about.