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

Dependently typed function:

f : (x : A) → B, where B may depend on x

Example

fromℕ : (n : ℕ) → Fin (suc n)
fromℕ zero = zero  -- Note: different zeros
fromℕ (suc n) = suc (fromℕ n)

Notes

• The dependent function spaces are called Π-types because the number of elements can be given as a product:
  ∣(x : A)→ B∣ = ∏x∈A ∣B∣, for example
  ∣(n : Fin m)→ Fin (suc n)∣ = (m + 1)!
• Polymorphic functions like (A : Set) → A → A are special cases of dependent functions.
• Non-dependent functions like A → B are special cases of dependent functions
  ((x : A) → B where B doesn't depend on x).

Exercises

Define a substraction with restricted domain:

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

Define 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 

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

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

Exercises

Define 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 element indexing.

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