```
module Types.functions where
open import Lang.dataStructures using (
; true; false;
Bool; List;
ℕ; two; three; four; five; six; seven; eight; nine; ten; zero; succ;
one_::_; [];
; 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:

```
: ∀ {i} → Set i → Set i
Fun₁ = A → A Fun₁ A
```

and a binary one as:

```
: ∀ {i} → Set i → Set i
Fun₂ = A → A → A Fun₂ A
```

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 = zero
divBy2 zero (succ zero) = one -- well...
divBy2 (succ (succ n)) = succ (divBy2 n) -- take 2 at a time and count as 1
divBy2
-- proof of a number being even
: ℕ → Set
even = ⊤
even zero (succ zero) = ⟂
even (succ (succ n)) = even n even
```

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

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

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:

```
: ∀ {i j} (A : Set i) (P : A → Set j) → Set (i ⊔ j)
Π = (x : A) → P x Π A P
```

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))
= λ x → g (f x)
g ∘ f
_∘′_ : ∀ {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))
= λ x → g (f x) g ○ f
```

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.

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

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

```
_$_ : ∀ {a b} {A : Set a} {B : A → Set b}
→ ((x : A) → B x)
→ ((x : A) → B x)
= f x f $ x
```

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:

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

```
_⟨_⟩_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
→ A
→ (A → B → C)
→ B
→ C
= f x y x ⟨ f ⟩ y
```

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

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

```
: ∀ {a} {A : Set a} → A → Set a
typeOf {A = A} _ = A typeOf
```

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