Simply-typed λ-calculus

The “hello world”: terms and types for the simply-typed λ-calculus, weak-head reduction, and a type checker that goes under binders with pi/==> and suspends on the holes of an incomplete term rather than guessing what they stand for.

The checker is picked up from here in Constraints: why matching rather than unifying is what lets it suspend, and how a constraint handling rule then rejects the holes that admit no consistent type.

../code/stlc.elpi:

% The "hello world" of lambda-tree syntax: simply-typed lambda calculus,
% weak-head reduction, and a type checker -- one that also handles terms with
% holes in them, by suspending on a hole instead of guessing its shape.

data term.
symb app term -> term -> term.
symb fun (term -> term) -> term.

data ty.
symb arr ty -> ty -> ty.

% weak-head reduction
func whd term -> term.
whd (app Hd Arg) Reduct :- whd Hd (fun F), !, whd (F Arg) Reduct.
whd X X.

% type checking
func of term -> ty.
of (app Hd Arg) B :- of Hd (arr A B), of Arg A.
of (fun F) (arr A B) :- pi x\ of x A ==> of (F x) B.
of (uvar as Hole) T :- declare_constraint (of Hole T) [Hole].

main :-
  Fst = fun (x\ fun y\ x),
  of Fst FstTy,
  print "type of Fst:" FstTy,

  Id = fun (z\ z),
  whd (app Fst Id) Reduct,
  print "\nwhd of Fst applied to the identity:" Reduct,

  ( of (fun (x\ app x x)) _
  ; print "\nfun (x\\ app x x) has no type: occur-check failure" ),

  of (app H _) AppTy,
  print "\nof (app H _): H still unknown, type" AppTy "-- of has suspended:",
  print_constraints,
  H = Id,
  print "\nafter H := the identity, one constraint resolved:",
  print_constraints.

type of Fst: arr X0 (arr X1 X0)

whd of Fst applied to the identity: fun c0 \ fun c1 \ c1

fun (x\ app x x) has no type: occur-check failure

of (app H _): H still unknown, type X2 -- of has suspended:
 of X3 X4  /* suspended on X3 */ of X5 (arr X4 X2)  /* suspended on X5 */

after H := the identity, one constraint resolved:
 of X3 X2  /* suspended on X3 */

Terms are HOAS (Terms): app pairs a function with its argument, fun carries an actual Elpi function term -> term, so λx.λy.x is fun (x\ fun y\ x), and applying that Elpi function is substitution, with no substitution code to write. Types have one constructor, arr, for the function space.

whd reduces a term to weak-head normal form: unfold app until the head is a fun, then β-reduce (apply the Elpi function) and keep going. Anything else is already in normal form.

of is the type checker. The rule for app is an ordinary Horn clause; the rule for fun needs a fresh name for the bound variable and a rule that only holds while checking under it, which is what pi/==> provide (Inference rules and queries, Logic Programming). Both whd and of are declared func, each with at most one result, and the determinacy checker (Determinacy checking) confirms it: whd’s two overlapping rules are kept apart by the cut, of’s three by their distinct heads.

Applying a term to itself, fun (x\ app x x), has no type: to type-check it, x’s type would have to be a function space with itself as the argument type, and the occur check (Unification and variables) rejects the resulting cyclic assignment.

The last rule of of is what makes the checker usable on a term that is still being built. of (uvar as Hole) T matches a bare unification variable, a hole, and instead of failing (no term to inspect) or looping (if the argument were unified rather than matched), it suspends: of Hole T becomes a constraint, keyed on Hole, to be retried once Hole is known. So of (app H _) AppTy with H unknown succeeds, AppTy left an unbound type, and two of goals suspended in the store. Assigning H the identity function wakes its constraint, which resolves; the goal still waiting on the argument now carries AppTy as that argument’s type, the identity having tied the two together.