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:

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