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