sml-hm

Hindley-Milner type inference (Algorithm W) for a mini-ML, in pure Standard ML. The language is the lambda calculus with let-polymorphism, integer and boolean literals, and if, over a small base environment of polymorphic primitives (pair/fst/snd, nil/cons, +, eq).

The pure lambda fragment is shared with the vendored sml-lambda library: ofLambda imports a Lambda.term (parsed by Lambda.parse) into the HM expression language, so a lambda term written in concrete syntax can be given its principal type.

Inference is sound and complete for HM: it returns the principal type, generalised at let, with full occurs-checked unification. tyToString renders a type with type variables renamed canonically ('a, 'b, … in order of first appearance), so principal types are reproducible and byte-identical across MLton and Poly/ML.

No FFI, no threads, no clock, no randomness.

API

structure Hm : sig
  datatype ty = TVar of int | TInt | TBool
    | TArrow of ty * ty | TPair of ty * ty | TList of ty
  datatype expr = Var of string | Lam of string * expr | App of expr * expr
    | Let of string * expr * expr | LitInt of int | LitBool of bool
    | If of expr * expr * expr
  exception TypeError of string

  val ofLambda   : Lambda.term -> expr
  val infer      : expr -> ty            (* principal type; raises TypeError *)
  val typeOf     : expr -> string        (* canonical pretty: "'a -> 'a" *)
  val typeable   : expr -> bool
  val tyToString : ty -> string          (* canonical variable renaming *)
end

Example

(* the K combinator *)
val "'a -> 'b -> 'a" = Hm.typeOf (Hm.Lam ("x", Hm.Lam ("y", Hm.Var "x")))

(* let-polymorphism: id used at two types *)
val "int * bool" =
  Hm.typeOf (Hm.Let ("id", Hm.Lam ("x", Hm.Var "x"),
    Hm.App (Hm.App (Hm.Var "pair", Hm.App (Hm.Var "id", Hm.LitInt 1)),
            Hm.App (Hm.Var "id", Hm.LitBool true))))

(* type a lambda term parsed by sml-lambda *)
val "('a -> 'a) -> 'a -> 'a" = Hm.typeOf (Hm.ofLambda (Lambda.church 2))

Running examples/demo.sml with make example prints:

Algorithm W principal types:

  I  = \x. x                         : 'a -> 'a
  K  = \x y. x                       : 'a -> 'b -> 'a
  S  = \f g x. f x (g x)             : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c
  compose = \f g x. f (g x)          : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
  let id = \x.x in pair (id 1) (id true) : int * bool
  \x. cons x nil                     : 'a -> 'a list

Let-polymorphism is required (these are ill-typed without it):

  self-application  \x. x x          : ILL-TYPED (occurs check)

Typing lambda terms parsed by sml-lambda:

  \x. x                : 'a -> 'a
  \f x. f x            : ('a -> 'b) -> 'a -> 'b
  church 2 = \f x. f (f x) : ('a -> 'a) -> 'a -> 'a

Build & test

Requires MLton and/or Poly/ML.

make test        # build + run the suite under MLton
make test-poly   # run the suite under Poly/ML
make all-tests   # both
make example     # build + run the demo
make clean

Installing with smlpkg

smlpkg add github.com/sjqtentacles/sml-hm
smlpkg sync

sml-hm vendors sml-lambda under lib/github.com/sjqtentacles/sml-lambda/ (a byte-identical copy of the upstream library). Reference lib/github.com/sjqtentacles/sml-hm/hm.mlb from your own .mlb (MLton / MLKit), or feed sources.mlb to tools/polybuild (Poly/ML).

Layout

sml.pkg                                   smlpkg manifest (requires sml-lambda)
Makefile                                  MLton + Poly/ML targets
.github/workflows/ci.yml                  CI: MLton + Poly/ML
lib/github.com/sjqtentacles/
  sml-hm/      hm.sig hm.sml sources.mlb hm.mlb
  sml-lambda/  vendored lambda-calculus library (byte-identical copy)
examples/
  demo.sml      principal types + sml-lambda bridge
test/
  harness.sml / test.sml                  27 reference checks
  entry.sml / main.sml
tools/polybuild                           Poly/ML build wrapper

Tests

27 deterministic checks: known principal types for the standard combinators (I, K, apply, compose, S), let-polymorphism (typable only with generalisation), literals/if/primitives, lists and pairs, classic untypable terms (self-application via the occurs check, a monomorphically λ-bound identifier used at two types, unbound variables, branch/arity mismatches), the ofLambda bridge typing terms parsed by sml-lambda (including Church numerals), and canonical type-variable rendering. Run make all-tests to verify identical output under both compilers.

License

MIT. See LICENSE.