vectors.agda

vectors.agda

module vectors where

-- For every inductive recursor:
--   d is the base case
--   e is the inductive step

--
-- Natural numbers
--
data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

natrec : {P : Set} → ℕ → P → (ℕ → P → P) → P

natrec zero     d e = d
natrec (succ n) d e = e n (natrec n d e)

--
-- Lists
--
data List (A : Set) : Set where
  listnil : List A
  listcons : A → List A → List A

listrec : {A P : Set} → List A → P → (A → List A → P → P) → P
listrec listnil        d e = d
listrec (listcons a l) d e = e a l (listrec l d e)

listmap : {A B : Set} -> (A -> B) -> List A -> List B
listmap f l = listrec l listnil (λ x y z → listcons (f x) z)

--
-- Vectors
--
data Vect (A : Set) : ℕ → Set where
  vectnil   : Vect A zero
  vectcons  : {n : ℕ} → A → Vect A n → Vect A (succ n)

vectrec : {A P : Set} → {n : ℕ} → Vect A n → P → ({m : ℕ} → A → Vect A m → P → P) → P
vectrec vectnil        d e = d
vectrec (vectcons a v) d e = e a v (vectrec v d e)

forgetlength : {A : Set} → {n : ℕ} → Vect A n → List A
forgetlength v = vectrec v listnil (λ x y z → listcons x z)

vectmap : {A B : Set} → {n : ℕ} → (A → B) → Vect A n → Vect B n
vectmap f (vectcons a v) = vectrec v vectnil (λ x y z → vectcons (f x) z)

data Vect (A : Set) : ℕ → Set where
  vectnil   : Vect A zero
  vectcons  : {n : ℕ} → A → Vect A n → Vect A (succ n)

vectrec : {A : Set}{P : ∀ {n} → Set} → {n : ℕ} → Vect A n → P {zero} → ({m : ℕ} → A → Vect A m → P {m} → P {succ m}) → P {n}
vectrec vectnil        d e = d
vectrec (vectcons a v) d e = e a v (vectrec v d e)


vectind : {A : Set}{P : ∀ {n} → Vect A n → Set} → {n : ℕ} → (xs : Vect A n) →
          P {zero} vectnil → ({m : ℕ} → (x : A) → (xs : Vect A m) → P {m} xs → P {succ m} (vectcons x xs)) → P {n} xs
vectind vectnil        d e = d
vectind (vectcons a v) d e = e a v (vectind v d e)

forgetlength : {A : Set} → {n : ℕ} → Vect A n → List A
forgetlength v = vectrec v listnil (λ x y z → listcons x z)

vectmap : {A B : Set} → {n : ℕ} → (A → B) → Vect A n → Vect B n
vectmap f v = vectrec {P = \ {n} → Vect _ n} v vectnil (λ x y z → vectcons (f x) z)

vectmap' : {A B : Set} → {n : ℕ} → (A → B) → Vect A n → Vect B n
vectmap' f v = vectind {P = \ {n} _ → Vect _ n} v vectnil (λ x y z → vectcons (f x) z)