Expressions

• x: variables
• 100: numbers
• #t|#f: the true and false literals
• (\|λ)x: t. e: a lambda expression with x bound to type t
• let x: t = e1 in e2: binds x to e1 and then evaluates e2
• f a: application to a lambda
• if e1 then e2 else e3: an if-then-else expression
• ref e: boxes e and returns a reference to it
• !r: unboxes the value at reference r
• r := e: places the value of e in the reference r

All type annotations of form : t are optional. If not specified, the type defaults to the unknown type ?. There is also the special type marker _, which instructs the compiler to infer a principal type.

Types

• ?: the unknown type, admitting any value
• _: mark type to be inferred
• nat: the type of natural numbers
• bool: the type of booleans
• t1 -> t2: function type
• ref t: a reference type

Builtin Functions

• succ: nat -> nat
  • succ n is n + 1
• pred: nat -> nat
  • pred n is n - 1
• add: nat -> nat -> nat
  • add m n is m + n
• mult: nat -> nat -> nat
  • mult m n is m * n
• eqn: nat -> nat -> bool
  • eqn m n is m == n
• eqb: bool -> bool -> bool
  • eqb b c is b == c

Full Parser Specification