Functions
Functions make up the backbone of the Vehicle language.
Function types
The function type is written A -> B
where A
is the input
type and B
is the output type.
For example Rat -> Bool
is the type of functions from
a rational number to a boolean value.
As is standard in functional languages, the function arrow associates to
the right so A -> B -> C
is therefore equivalent to A -> (B -> C)
.
The type A -> (B -> C)
is a function that takes something of type A
and returns a function from B to C.
In contrast (A -> B) -> C
is a function that takes another function
from A -> B
as its first argument and returns something of type C
.
Function application
As in most functional languages, function application is written
by juxtaposition of the function with its arguments. For example, given
a function f
of type Rat -> Bool -> Rat
and arguments x
of
type Rat
and y
of type Bool
, the application of f
to x
and y
is written f x y
and this expression has type Bool
.
This is unlike imperative languages such as Python, C or Java where
you would write f(x,y)
.
Function declarations
Declarations may be used to define new functions. A declaration is of the form
<name> : <type>
<name> [<args>] = <expr>
For example the function increment
that takes adds 1
to a natural number may be
defined as follows:
increment : Nat -> Nat
increment x = x + 1
and can then be used later in the specification.
Lambdas
Alternatively, anonymous functions can be declared using the
\x -> ...
notation, e.g.
\x -> x + 1
is also a function that increments its input. Lambda functions can be applied in the same way as normal, for example:
(\x -> x + 1) 1
will evaluate to 2
.
Variables bound by lambdas may optionally be annotated by their type as follows:
\(x : Nat) -> x + 1
Multiple parameter lambdas are also supported:
\x y -> x + 2 * y