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`

:

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

we could also use a wildcard type (`_`

) like this:

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

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
= whatever -- true AND whatever is whatever
true ∧ whatever = false -- false AND whatever is false
false ∧ whatever
infixr 6 _∧_
```

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

These functions can be applied as:

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

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

```
_+_ : ℕ → ℕ → ℕ
= n
zero + n = succ (m + n)
succ m + n
infixl 6 _+_
```

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

```
= ten + one
eleven = eleven + one
twelve = twelve + one thirteen
```

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

```
: List ⊤ → ℕ
length = zero
length [] (x :: xs) = one + (length xs) length
```

Dependent pair types are a pair of two types such that the second type is a function of the first type:

```
data Σ (A : Set) (B : A → Set) : Set where
_,_ : (a : A) → (b : B a) → Σ A B
```

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:

`= \ (A : Set)(x : A) → x example₁ `

and a more concise syntax:

`= λ A x → x example₂ `

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:

```
data Square : ℕ → Set where
: (m : ℕ) → Square (m × m) sq
```

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:

```
: (n : ℕ) → Square n → ℕ
root .(m × m) (sq m) = m root
```

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

```
: {A B : Set} → List A → (A → B) → List B
map = []
map [] f (x :: xs) f = (f x) :: (map xs f) map
```

Here, we apply the function `addOne`

to a list, using `map`

:

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

```
: ((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)
prop₅ → e) is-the-same-as (\x → (\y → e))
(\x y -the-same-as ((f a) b) (f a b) is
```