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 (_×_; _,_)

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`

Define a subtraction with a restricted domain.

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

Define a conversion from

`Fin n`

to`ℕ`

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

Define

`fromℕ≤`

such that`toℕ (fromℕ≤ e)`

is`m`

if`e : m < n`

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

Define

`inject+`

such that`toℕ (inject+ n i)`

is the same as`toℕ i`

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

Define

`four`

such that`toℕ four`

is`4`

:`four : Fin 66`

Define

`raise`

such that`toℕ (raise n i)`

is the same as`n + toℕ i`

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

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`

Define concatenation for vectors.

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

Define

`maps`

. (Note that two cases will be enough.)`maps : ∀ {n}{A B : Set} → Vec (A → B) n → Vec A n → Vec B n`

Define

`replicate`

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

Define

`map`

with the help of`maps`

and`replicate`

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

Define

`zip`

with the help of`map`

and`maps`

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

Define (safe, total) element indexing.

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