module Data.Vec.Base where

VectorsπŸ”—

The type Vec is a representation of n-ary tuples with coordinates drawn from A. Therefore, it is equivalent to the type i.e., the functions from the standard finite set with elements to the type The halves of this equivalence are called lookup and tabulate.

data Vec {β„“} (A : Type β„“) : Nat β†’ Type β„“ where
  []  : Vec A zero
  _∷_ : βˆ€ {n} β†’ A β†’ Vec A n β†’ Vec A (suc n)

Vec-elim
  : βˆ€ {β„“ β„“'} {A : Type β„“} (P : βˆ€ {n} β†’ Vec A n β†’ Type β„“')
  β†’ P []
  β†’ (βˆ€ {n} x (xs : Vec A n) β†’ P xs β†’ P (x ∷ xs))
  β†’ βˆ€ {n} (xs : Vec A n) β†’ P xs
Vec-elim P p[] p∷ [] = p[]
Vec-elim P p[] p∷ (x ∷ xs) = p∷ x xs (Vec-elim P p[] p∷ xs)

infixr 20 _∷_

private variable
  β„“ : Level
  A B C : Type β„“
  n k : Nat

lookup : Vec A n β†’ Fin n β†’ A
lookup (x ∷ xs) fzero = x
lookup (x ∷ xs) (fsuc i) = lookup xs i
tabulate : (Fin n β†’ A) β†’ Vec A n
tabulate {zero} f  = []
tabulate {suc n} f = f fzero ∷ tabulate (Ξ» x β†’ f (fsuc x))

map : (A β†’ B) β†’ Vec A n β†’ Vec B n
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

zip-with : (A β†’ B β†’ C) β†’ Vec A n β†’ Vec B n β†’ Vec C n
zip-with f [] [] = []
zip-with f (x ∷ xs) (y ∷ ys) = f x y ∷ zip-with f xs ys

replicate : (n : Nat) β†’ A β†’ Vec A n
replicate zero a = []
replicate (suc n) a = a ∷ replicate n a

instance
  From-prod-Vec : From-product A (Vec A)
  From-prod-Vec .From-product.from-prod = go where
    go : βˆ€ n β†’ Vecβ‚“ A n β†’ Vec A n
    go zero xs                = []
    go (suc zero) xs          = xs ∷ []
    go (suc (suc n)) (x , xs) = x ∷ go (suc n) xs

_ : Path (Vec Nat 3) [ 1 , 2 , 3 ] (1 ∷ 2 ∷ 3 ∷ [])
_ = refl