Lambda the Ultimate

Typer: ML boosted with type theory and Scheme

Abstract
We present the language Typer which is a programming language in the ML family. Its
name is an homage to Scheme(r) with which it shares the design of a minimal core language
combined with powerful metaprogramming facilities, pushing as much functionality as
possible into libraries. Contrary to Scheme, its syntax includes traditional infix notation,
and its core language is very much statically typed. More specifically the core language is a
variant of the implicit calculus of constructions (ICC). We present the main elements of the
language, including its Lisp-style syntactic structure, its elaboration phase which combines
macro-expansion and Hindley-Milner type inference, its treatment of implicit arguments,
and its novel approach to impredicativity.