Functions

Functions make up the backbone of the language. Function application is written by juxtaposition, i.e. f x represents the function f applied to input x.

The function type is written A -> B where A is the input type and B is the output type. For example Tensor Rat [10,10] -> Bool is the type of functions from 10 x 10 matrix of rational numbers to a single boolean value. As is standard in functional languages, the function arrow associates to the right so A -> B -> C stands for A -> (B -> C).

New functions can be introduced in two ways. Firstly, anonymous lambda functions can be declared using the \x -> notation, e.g.

\x -> x + 2

is a function that adds 2 to its input. Alternatively, the same function could be given a name and an explicit type as follows:

add2 : Nat -> Nat
add2 x = x + 2

and can then be used later in the specification by referring to this name.