# Import list

```
module Functions.Dependent where

open import Data.Nat using (ℕ; zero; suc; _+_; z≤n; s≤s; _<_)
open import Data.Fin using (Fin; zero; suc)
open import Data.Vec using (Vec; []; _∷_)
open import Data.Product using (_×_; _,_)```

# Dependently typed functions

We call the function `f : (x : A) → B` dependently-typed if `B` (set) may depend on `x` (value).

For example, consider the following:

```
fromℕ : (n : ℕ) → Fin (suc n)
fromℕ zero    = zero            -- Note: this is a different zero!
fromℕ (suc n) = suc (fromℕ n)```

Remarks:

• The spaces of dependent functions are called `Π`-types because the number of their elements could be given as a product, that is:

`(x : A) → B` ∣ = ∏(`x``A`) ∣`B`

For example:

`(n : Fin m) → Fin (suc n)` ∣ = (`m` + 1)!

• Polymorphic functions, such as `(A : Set) → A → A` are special cases for dependent functions.

• Non-dependent functions, such as `A → B` are only special cases for dependent functions, that is:

`(x : A) → B` where `B` does not depend on `x`, so it is `A → B`

## Exercises

1. Define a subtraction with a restricted domain.

`_-_ : (n : ℕ) → Fin (suc n) → ℕ`

2. Define a conversion from `Fin n` to `ℕ`.

`toℕ : ∀ {n} → Fin n → ℕ`

3. Define `fromℕ≤` such that `toℕ (fromℕ≤ e)` is `m` if `e : m < n`.

`fromℕ≤ : ∀ {m n} → m < n → Fin n`

4. Define `inject+` such that `toℕ (inject+ n i)` is the same as `toℕ i`.

`inject+ : ∀ {m} n → Fin m → Fin (m + n)`

5. Define `four` such that `toℕ four` is `4`:

`four : Fin 66`

6. Define `raise` such that `toℕ (raise n i)` is the same as `n + toℕ i`:

`raise : ∀ {m} n → Fin m → Fin (n + m)`

7. Define (a safe, total version of) `head` and `tail`.

`head : ∀ {n}{A : Set} → Vec A (suc n) → A`
`tail : ∀ {n}{A : Set} → Vec A (suc n) → Vec A n`

8. Define concatenation for vectors.

`_++_ : ∀ {n m}{A : Set} → Vec A n → Vec A m → Vec A (n + m)`

9. Define `maps`. (Note that two cases will be enough.)

`maps : ∀ {n}{A B : Set} → Vec (A → B) n → Vec A n → Vec B n`

10. Define `replicate`.

`replicate : ∀ {n}{A : Set} → A → Vec A n`

11. Define `map` with the help of `maps` and `replicate`.

`map : ∀ {n}{A B : Set} → (A → B) → Vec A n → Vec B n`

12. Define `zip` with the help of `map` and `maps`.

`zip : ∀ {n}{A B : Set} → Vec A n → Vec B n → Vec (A × B) n`

13. Define (safe, total) element indexing.

`_!_ : ∀ {n}{A : Set} → Vec A n → Fin n → A`