# 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
```