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 head : Vec A (suc n) β A head (x β· xs) = x tail : Vec A (suc n) β Vec A n tail (x β· xs) = xs lookup : Vec A n β Fin n β A lookup xs n with fin-view n ... | zero = head xs ... | suc i = lookup (tail xs) i
Vec-cast : {x y : Nat} β x β‘ y β Vec A x β Vec A y Vec-cast {A = A} {x = x} {y = y} p xs = Vec-elim (Ξ» {n} _ β (y : Nat) β n β‘ y β Vec A y) (Ξ» { zero _ β [] ; (suc x) p β absurd (zeroβ suc p) }) (Ξ» { {n} head tail cast-tail zero 1+n=len β absurd (sucβ zero 1+n=len) ; {n} head tail cast-tail (suc len) 1+n=len β head β· cast-tail len (suc-inj 1+n=len) }) xs y p
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 _++_ : β {n k} β Vec A n β Vec A k β Vec A (n + k) [] ++ ys = ys (x β· xs) ++ ys = x β· (xs ++ ys) 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