module Vector where

open import Nat
open import Product
open import Unit

-- "vectors" of a certain length (dimension), a polymorphic dependent type
-- an "inductive family"

data Vec (A : Set) : Nat -> Set where
  []   : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (succ n)

-- type and term constructors are
-- Vec : Set -> Nat -> Set
-- [] : {A : Set} -> Vec A zero
-- _::_ : {A : Set} -> {n : Nat} -> A -> Vec A n -> Vec A (succ n)

-- now we can express that head and tail are only defined for non-empty lists

head : {A : Set} {n : Nat} -> Vec A (succ n) -> A
head (x :: _) = x

tail : {A : Set} {n : Nat} -> Vec A (succ n) -> Vec A n
tail (_ :: xs) = xs

-- map preserves the lenght of a list:

map : {A B : Set} -> {n : Nat} -> (A -> B) -> Vec A n -> Vec B n
map f []        = []
map f (x :: xs) = f x :: map f xs

-- the both input and output lists of zip are equally long

zip : {A B : Set} -> {n : Nat} -> Vec A n -> Vec B n -> Vec (A × B) n
zip []        []        = []
zip (x :: xs) (y :: ys) = < x , y > :: zip xs ys

-- Vec as a "recursive family"

VecRec : Set → Nat → Set
VecRec A zero     = Unit
VecRec A (succ n) = A × (VecRec A n)

headRec : {A : Set} → (n : Nat) -> Vec A (succ n) -> A
headRec n (x :: _) = x