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”.

```
{-# OPTIONS --allow-unsolved-metas #-}
module Lang.functions where
open import Lang.dataStructures hiding (_+_)
```

Syntax for defining functions in Agda:

- Define name and type of function
- Define clauses for each applicable pattern

```
-- 1. Name (not), Type (Bool → Bool)
not : Bool → Bool
-- 2. Clause 1: if the argument to `not` is `true`
not true = false
-- 2. Clause 2: if the argument to `not` is `false`
not false = true
```

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

In Agda, function names containing `_`

s indicate those functions can behave as operators. Hence `_+_`

indicates that instead of calling the functions `+(a, b)`

one can call it as `a + b`

, whereas `if_then_else_`

can be called as `if condition then 2 else 3`

.

One has to also define whether the infix operator is left or right associative (`infixl`

, `infixr`

) and its precedence level. The default precedence level for a newly defined operator is 20.

```
_∧_ : 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:

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

Similar to dependent pair types, a dependent function type is a function type whose result type depends upon its argument value. The notation in type theory looks like this for binary dependent function types:

\[ \prod_{x : A} B(x) \]

with ternary dependent pair types being represented as:

\[ \prod_{x : A} \prod_{y : B(x)} C(y) \]

and so on.

Lambda or anonymous functions can be defined using the following syntax:

and a more concise syntax:

`example₂ = λ A x → x`

Note that `\`

and `λ`

can be used interchangeably.

Following are a few examples of functions:

Functions in Agda can work with implicit parameters. For example, instead of having the specify the type of `A`

, the compiler can be expected to figure it out. Hence instead of defining `_++_ : (A : Set) → List A → List A → List A`

, we define it like:

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

Note that the curly braces `{}`

are “implicit arguments” in Agda. Values of implicit arguments are derived from other arguments’ (in this case `List A`

) 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 passed like `function_name{A = A}`

).

This function takes a type as a parameter `A`

, and hence can work on `List`

s of any type `A`

. This feature of functions is called “parametric polymorphism”.

A dot pattern (also called inaccessible pattern) can be used when the only type-correct value of the argument is determined by the patterns given for the other arguments. The syntax for a dot pattern is `.t`

.

As an example, consider the datatype `Square`

defined as follows:

Suppose we want to define a function `root : (n : ℕ) → Square n → ℕ`

that takes as its arguments a number `n`

and a proof that it is a square, and returns the square root of that number. We can do so as follows:

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

```
prop₁ : ((x : A) (y : B) → C) is-the-same-as ((x : A) → (y : B) → C)
prop₂ : ((x y : A) → C) is-the-same-as ((x : A)(y : A) → C)
prop₃ : (forall (x : A) → C) is-the-same-as ((x : A) → C)
prop₄ : (forall x → C) is-the-same-as ((x : _) → C)
prop₅ : (forall x y → C) is-the-same-as (forall x → forall y → C)
(\x y → e) is-the-same-as (\x → (\y → e))
(f a b) is-the-same-as ((f a) b)
```