lambda

A collection of interpreters, type checkers, and REPLs implemented in Haskell. Currently, the following languages are supported:

• Untyped lambda calculus
• SK combinator calculus
• System F
• Hindley-Milner type system
• Calculus of constructions

You can access the different REPLs by passing an argument to the executable: "lambda", "sk", "systemf", "hm", or "coc". For more information, see the manual below.

Untyped lambda calculus

When you enter a term, the interpreter will reduce it to βη-normal form if possible, and display the result. You can use \ instead of λ for abstractions.

> (\b. \c. b c (\x. \y. y)) (\x. \y. x) (\x. \y. y)
λx. λy. y

You can also define named constants using =.

> true = \x. \y. x
> false = \x. \y. y
> and = \b. \c. b c false
> and true false
λx. λy. y

When you define a constant, it is added as an argument to all succeeding inputs. In the example above, when the user types and true false, the interpreter evaluates the expression (λtrue. (λfalse. (λand. and true false) (λb. λc. b c false)) (λx. λy. y)) (λx. λy. x).

Any sequence of basic latin letters and/or digits is a valid variable. For example, x, 0, Abc, and add1 can all be used as variables.

SK combinator calculus

SK combinator calculus is a restricted version of lambda calculus. It has variables and application, but no λ-abstraction. There are two variables with a special meaning: s and k. sxyz reduces to xz(yz), and kxy reduces to x (where x, y, and z stand for any terms). Variables are limited to a single character, so you don't need to put spaces between them.

> s(s(skk)(kx))(ky)z
zxy

You can define named constants using =.

> i = skk
> f = ki
> a = ss(k(kf))
> afk
k(skk)

System F

System F is a typed lambda calculus with universal quantifiers. There are separate syntaxes for terms (e) and types (τ):

e ::= x         variable
    | λx:τ. e   term abstraction
    | λα. e     type abstraction
    | e e       term application
    | e [τ]     type application

τ ::= α         type variable
    | τ → τ     function type
    | ∀α. τ     universal quantifier

In the REPL, you can use \, ->, and ? instead of λ, →, and ∀ respectively. You can also create local variables using the syntax {x = e1} e2. This is equivalent to (λx:τ. e2) e1, where τ is the type of e1.

When you enter a well-typed term in the REPL, the term is compiled into the untyped lambda calculus by removing all type annotations. It is then reduced to βη-normal form and printed.

> (\a. \x:a. x) [?a. a -> a -> a] (\a. \x:a. \y:a. x)
: ∀a. a → a → a
λx. λy. x
> (\a. \x:a. x) [?a. a -> a] (\a. \x:a. \y:a. x)
could not match types:
* ∀a. a → a
* ∀a. a → a → a

You can define named constants using =. When you type x = e in the REPL, the interpreter adds {x = e} before all succeeding inputs. You can also define type synonyms using ~.

> nat ~ ?a. (a -> a) -> a -> a
> 0 = \a. \f:a -> a. \x:a. x
> S = \n:nat. \a. \f:a -> a. \x:a. f (n [a] f x)
> add = \n:nat. \k:nat. n [nat] S k
> add (S (S 0)) (S (S (S 0)))
: ∀a. (a → a) → a → a
λf. λx_1. f (f (f (f (f x_1))))

Hindley-Milner type system

Hindley-Milner is a type system that allows a restricted form of parametric polymorphism while not requiring any type annotations; the type of an expression can always be inferred. Terms (e) and types (τ) are constructed as follows:

e ::= k           constant
    | x           variable
    | {x = e} e   local definition
    | λx. e       abstraction
    | e e         application

τ ::= ι           type constant
    | τ → τ       function type
    | α           type variable

Universal quantifiers are not allowed within function types. Therefore, booleans, numbers, and data structures cannot be encoded in the usual way, and must be built in to the calculus itself. My implementation includes the following type constants (ι) and term constants (k):

ι ::= Int | Bool

k ::= true | false                  : Bool
    | 0 | 1 | ...                   : Int
    | and | or                      : Bool → Bool → Bool
    | not                           : Bool → Bool
    | if                            : Bool → α → α → α
    | add | sub | mul | div | mod   : Int → Int → Int
    | eq | lt | gt                  : Int → Int → Bool

When you enter a term in the REPL, the interpreter prints the inferred type, and then reduces the term to normal form. Type variables are indexed by natural numbers; for example, the type of the identity function is displayed as 0 → 0 or 1 → 1 etc.

> add -2 5
: Int
3
> (\b. \x. if b (add x 1) (sub x 1)) true 5
: Int
6
> \x. \f. f true x
: 0 → (Bool → 0 → 3) → 3
λx. λf. f true x
> (\x. x) false 1
cannot unify types:
* Bool
* Int → 2

As in the other REPLs, you can define named constants using =.

Calculus of constructions

The calculus of constructions is a typed lambda calculus where the set of types is included in the set of terms. Terms are constructed as follows:

e ::= T               impredicative sort
    | T1 | T2 | ...   predicative sort
    | x               variable
    | λx:e. e         abstraction
    | ∀x:e. e         dependent product
    | e e             application

• The impredicative sort T is also written T0.
• In the REPL, you can use \ and ? instead of λ and ∀ respectively.
• If a bound variable is never used, you can replace it with an underscore, e.g. λ_:e. e or ∀_:e. e
• As a notational shorthand, you can write a → b or a -> b instead of ∀_:a. b.

Informally, the typing rules can be described as follows:

• T0 : T1, T1 : T2, T2 : T3, and so on.
• If x : Ti, then x : T(i + 1), for all natural numbers i. (In other words, each sort is a supertype of the previous sort.)
• If e : b, then (λx:a. e) : (∀x:a. b).
• If a : Ti and b : T0, then (∀x:a. b) : T0.
• If a : Ti and b : Tj (where j > 0), then (∀x:a. b) : T(max(i, j)).
• If f : (∀x:a. b) and e : a, then f e : b[e/x].

Anything that is possible in System F is also possible in CoC. In particular, one can work with data types via their church encodings.

> nat = ?a:T. (a -> a) -> a -> a
> 0 = \a:T. \f:(a -> a). \x:a. x
> S = \n:nat. \a:T. \f:(a -> a). \x:a. f (n a f x)
> add = \n:nat. \k:nat. n nat S k
> add (S (S 0)) (S (S (S 0)))
: ∀a:T. (a → a) → a → a
λa:T. λf:(a → a). λx:a. f (f (f (f (f x))))

Unlike in System F, one can define type constructors (functions from types to types), and higher-order type constructors (functions from type constructors to types). In the example below, vec : natT → T → T is a higher-order type constructor; vec n a creates the cartesian product of a with itself n times.

> natT = (T -> T) -> T -> T
> 0T = \f:(T -> T). \a:T. a
> ST = \n:natT. \f:(T -> T). \a:T. f (n f a)
> unit = ?a:T. a -> a
> pair = \a:T. \b:T. ?c:T. (a -> b -> c) -> c
> vec = \n:natT. \a:T. n (pair a) unit

Without inductive types, it is impossible to create non-trivial functions of type nat → a, where a has type T1 or greater. Therefore, to define vec, one must create a higher-level natural numbers type (called natT above).