```
module Types.functions where
open import Lang.dataStructures using (
Bool; true; false;
ℕ; List;
one; two; three; four; five; six; seven; eight; nine; ten; zero; succ;
_::_; [];
⊤; singleton; ⟂)
open import Agda.Primitive using (Level; _⊔_; lsuc)
open import Types.product using (Σ; _,_; fst; snd)
```

We have previously looked at how functions are defined in Agda. Here we will look at some abstract representations of functions and their properties.

A unary function is defined as:

and a binary one as:

In Type Theory, a function is also a type, called a **function type** represented as the type `Input₁ → Input₂ → ... → Inputₙ → Output`

, where `Inputᵢ`

are the input types and `Output`

is the output type. A function type `f : A → B`

can also be considered to be an exponential `f : Bᴬ`

and can be thought of as belonging to the set of all `b ∈ B`

that can be obtained from any `a ∈ A`

, hence `Bᴬ`

such elements.

The concept of **currying** can be explained using this representation as \(C^{A × B} = (C^A)^B\) hence a function taking multiple arguments `f : (A, B) → C`

is the same as `f : A → B → C`

. **Partial functions** can then be trivally described as functions that return functions with lesser number of arguments, or **arity**: `∀ a ∈ A, g = f(a) : B → C`

.

Dependent function types or Π-types are functions whose type of second argument depends upon the type of first.

i.e. function `f : A → (g A) → Set`

where `g : A → B`

.

In the notation of lambda abstraction:

\[ λx. (λx.y).ϕ \]

Another notation is to use \(\Pi_{x : A} B(x)\), mostly used in type theory to denote Π-types. Functions of higher arity then take the form \(\Pi_{x : A}\Pi_{y : B(x)} D(y)\) and so on.

To show how to use this type, we construct an example:

```
-- divide by 2
divBy2 : ℕ → ℕ
divBy2 zero = zero
divBy2 (succ zero) = one -- well...
divBy2 (succ (succ n)) = succ (divBy2 n) -- take 2 at a time and count as 1
-- proof of a number being even
even : ℕ → Set
even zero = ⊤
even (succ zero) = ⟂
even (succ (succ n)) = even n
```

Now, we can define a function that divides only even numbers by 2:

```
divBy2₂ : (n : ℕ) → even n → ℕ
divBy2₂ zero p = zero
divBy2₂ (succ zero) ()
divBy2₂ (succ (succ y)) p = succ (divBy2₂ y p)
```

In order to be applied, `divBy2₂`

requries its input `n`

to conform to the type `even n`

, which can only exist if the number `n`

is even! This makes `divBy2₂`

a dependent function.

A dependent Π-type can be constructively defined as:

A function composition is defined as:

```
_∘_ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c}
→ (g : {x : A} (y : B x) → C y)
→ (f : (x : A) → B x)
→ ((x : A) → C (f x))
g ∘ f = λ x → g (f x)
_∘′_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
→ (B → C)
→ (A → B)
→ (A → C)
f ∘′ g = _∘_ f g
```

and specifically for dependent types:

```
_○_ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : (x : A) → B x → Set c}
→ (g : {x : A} → Π (B x) (C x))
→ (f : Π A B)
→ Π A (λ x → C x (f x))
g ○ f = λ x → g (f x)
```

Going further, we define our machinery on all functions, dependent or not. However, it is worth nothing that by functions, we mean **pure functions**, i.e. without any side effects, for example IO, state manipulation, etc.

```
id : ∀ {a} {A : Set a} → A → A
id x = x
const : ∀ {a b} {A : Set a} {B : Set b} → A → B → A
const x = λ _ → x
```

A function application is a type which actually applies a bunch of arguments to a function.

Currying, as we saw earlier, converts a function that takes multiple arguments into a sequence of functions each taking one argument. Un-currying is the opposite of currying. We define both for binary functions, though further extensions are trivial:

```
curry : ∀ {i j k} {A : Set i} {B : A → Set j} {C : Σ A B → Set k}
→ (∀ s → C s)
→ (∀ x y → C (x , y))
curry f x y = f (x , y)
uncurry : ∀ {i j k} {A : Set i} {B : A → Set j} {C : ∀ x → B x → Set k}
→ (∀ x y → C x y)
→ (∀ s → C (fst s) (snd s))
uncurry f (x , y) = f x y
```

```
flip : ∀ {a b c} {A : Set a} {B : Set b} {C : A → B → Set c}
→ ((x : A) (y : B) → C x y)
→ ((y : B) (x : A) → C x y)
flip f = λ y x → f x y
```

```
_on_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
→ (B → B → C)
→ (A → B)
→ (A → A → C)
_*_ on f = λ x y → f x * f y
```

```
infix 0 case_return_of_ case_of_
case_return_of_ :
∀ {a b} {A : Set a}
(x : A) (B : A → Set b) → ((x : A) → B x) → B x
case x return B of f = f x
case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = case x return _ of f
```