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.