sml-lambda

The untyped lambda calculus plus the simply-typed lambda calculus (STLC), in pure Standard ML: a parser and pretty-printer, free variables, capture-avoiding substitution, alpha-equivalence, normal-order reduction with a step cap, Church numerals, and an STLC typechecker.

datatype term = Var of string | Lam of string * term | App of term * term

Dependency-free by design. The parser is a small hand-rolled recursive-descent parser living inside the library — no external parser-combinator package is vendored. No FFI, threads, clock or randomness: deterministic and identical under MLton and Poly/ML. Fresh-variable generation for substitution uses a deterministic primed-name scheme.

Concrete syntax

parse accepts both styles of binder:

• \x. x y (backslash + .)
• fn x => x y (fn + =>)

Consecutive binders may be grouped: \x y. t abbreviates \x. \y. t. Application is left-associative (x y z is (x y) z) and a lambda's body extends as far right as possible. A lambda in argument position must be parenthesised, e.g. f (\x. x).

Reduction

betaStep performs one normal-order (leftmost-outermost) reduction, reducing under lambdas once the spine is normal. normalize cap t iterates it up to cap steps and returns NONE if the cap is reached — so divergent terms such as (\x. x x) (\x. x x) terminate with NONE rather than looping.

API

structure Lambda : sig
  datatype term = Var of string | Lam of string * term | App of term * term
  exception Parse of string

  val parse     : string -> term
  val pretty    : term -> string
  val freeVars  : term -> string list
  val isClosed  : term -> bool
  val subst     : string -> term -> term -> term     (* t[x := s] *)
  val alphaEq   : term -> term -> bool
  val betaStep  : term -> term option
  val normalize : int -> term -> term option          (* step-capped *)
  val church    : int -> term

  structure Stlc : sig
    datatype ty = TVar | Base of string | Arrow of ty * ty
    datatype tm = V of string | Lam of string * ty * tm | App of tm * tm
    type context = (string * ty) list
    val tyEq       : ty -> ty -> bool
    val tyToString : ty -> string
    val typecheck  : context -> tm -> ty option
  end
end

Example

val SOME y = Lambda.normalize 100 (Lambda.parse "(\\x. x) y")     (* -> Var "y" *)

val succ = Lambda.parse "\\n f x. f (n f x)"
val two  = Lambda.normalize 100 (Lambda.App (succ, Lambda.church 1))
val true = Lambda.alphaEq (valOf two) (Lambda.church 2)            (* succ 1 = 2 *)

(* STLC: identity is a -> a; self-application is untypeable *)
val SOME _ = Lambda.Stlc.typecheck [] (Lambda.Stlc.Lam ("x", Lambda.Stlc.Base "a", Lambda.Stlc.V "x"))
val NONE   = Lambda.Stlc.typecheck []
               (Lambda.Stlc.Lam ("x", Lambda.Stlc.Base "a",
                  Lambda.Stlc.App (Lambda.Stlc.V "x", Lambda.Stlc.V "x")))

Running examples/demo.sml with make example prints:

Normal-order reduction (untyped):
  (\x. x) y  ~~>  y
  (\x y. x) a b  ~~>  a
  S K K a  ~~>  a

Church numerals  (succ = \n f x. f (n f x)):
  succ (church 1) = \f x. f (f x)
  alpha-equal to church 2? true

Simply-typed lambda calculus:
  \x:a. x       :  a -> a
  \x:a. x x     :  ill-typed (no finite type)
  \f:a->b. \x:a. f x :  (a -> b) -> a -> b

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-lambda
smlpkg sync

Reference lib/github.com/sjqtentacles/sml-lambda/lambda.mlb from your own .mlb (MLton / MLKit), or feed sources.mlb to tools/polybuild (Poly/ML).

Layout

sml.pkg                                   smlpkg manifest
Makefile                                  MLton + Poly/ML targets
.github/workflows/ci.yml                  CI: MLton + Poly/ML
lib/github.com/sjqtentacles/sml-lambda/
  lambda.sig   LAMBDA signature
  lambda.sml   parser + reduction + STLC typechecker
  sources.mlb / lambda.mlb
examples/
  demo.sml     reduction, Church numerals, STLC typing
test/
  harness.sml / test.sml                  58 reference checks
  entry.sml / main.sml
tools/polybuild                           Poly/ML build wrapper

Tests

58 deterministic checks: parser structure (both binder styles, grouped binders, left-associative application, right-extending bodies, parenthesised lambda arguments) and parse errors; pretty-printing with a parse ∘ pretty alpha-equality round-trip; freeVars/isClosed; capture-avoiding subst (including the classic (\y. x)[x := y] rename); alphaEq; normal-order betaStep/normalize with the (\x. x) y → y and K a b → a vectors and the omega divergence cap; Church numerals (succ (church 1) = church 2); the S K K = I combinator identity; and the STLC typechecker (\x:a. x : a -> a, self-application untypeable, application well-/ill-typing, context lookup, tyToString). Run make all-tests to verify identical output under both compilers.

License

MIT. See LICENSE.