A function `𝕗`

which takes a value of type `𝔸`

and returns a value of type `𝔹`

, is said to be of type `𝔸 → 𝔹`

and is written as `𝕗 : 𝔸 → 𝔹`

. The type `𝔸`

is called the function `𝕗`

’s “domain” and `𝔹`

is the “co-domain”. Functions are allowed to be recursive, in fact, in Agda we make heavy use of recursion and pattern matching while defining functions.

Following are a few examples of functions:

The simplest of functions simply match patterns. For example the function for `not`

:

```
not : Bool → Bool
not true = false -- return false if we are given a true
not false = true -- return a true if we are given a false
```

we could also use wildcard type like this:

```
not₁ : Bool → Bool
not₁ true = false -- return false if we are given a true
not₁ _ = true -- return true in all other cases
```

```
_∧_ : Bool → Bool → Bool
true ∧ whatever = whatever -- true AND whatever is whatever
false ∧ whatever = false -- false AND whatever is false
infixr 6 _∧_
```

```
_∨_ : Bool → Bool → Bool
true ∨ whatever = true -- true or whatever is true
false ∨ whatever = whatever -- false or whatever is whatever
infixr 6 _∨_
```

These functions can be applied as:

```
notTrue : Bool
notTrue = not true
false₁ : Bool
false₁ = true ∧ false
true₁ : Bool
true₁ = true ∨ false ∨ false₁
```

Here we follow a similar pattern as in `data`

, we define:

- the identity condition, what happens on addition with zero in this case
- and how to successively build up the final value

Thus, we can use them to get new numbers easily:

Functions in Agda can take types as parameters such that the function can work on all higher types of that type parameter. This function takes a type as a parameter `A`

, and hence can work on `List`

s of any type `A`

.

```
_++_ : {A : Set} → List A → List A → List A
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)
infixr 5 _++_
```

This feature of functions is called “parametric polymorphism”. This function works on higher levels of abstraction, i.e. on all list types.

Note that the curly braces `{}`

are called “implicit arguments” in Agda. Values of implicit arguments are derived from other arguments’ values and types by solving type equations. You don’t have to apply them or pattern match on them explicitly (though they can be explicitly stated like `{A = A}`

).

The length of a list consists of traversing through the list and adding one for each element:

We implement the `map`

function, of “map-reduce” fame, for `List`

s: A map function for a `List`

is a function that applies a lambda (un-named) function to all elements of a `List`

.

If `f`

were a lambda function, map-ing `f`

over `List(a, b, c, d)`

would produce `List(f(a), f(b), f(c), f(d))`

Here, we apply the function `addOne`

to a list, using `map`

:

```
addOne : ℕ → ℕ
addOne x = x + one
oneAdded : List ℕ
oneAdded = map (one :: two :: three :: four :: []) addOne
```