Language syntax

Abstractions:

\x:T.e

Where x is an identifier, T a type, and e an expression

Aplication:

lhs rhs

Where lhs and rhs are expressions

Variable:

x

Where x is an identifier

Constants:

n

where n is an number

or

true

or

false

Types

The language has the primitive types Bool and Nat, and arrow types of the form T1 -> T2, where multiple of these can be composed, and parentesis can be used to specify associativity, ex: (Nat -> Nat) -> Nat -> Nat

Using the repl

When entering a valid expression into the repl, it will be type checked, and if well typed, its beta reduced form and type is printed.

The repl offers additional commands starting with :, the following commands are availaibe

• :t expr: get the type of expr, but do not beta reduce
• :ctx ident : T: add a variable identfied by ident of type T to the type checking context, arrow types need to be in parentesis