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 : Type β n k : Nat lookup : Vec A n β Fin n β A lookup (x β· xs) fzero = x lookup (x β· xs) (fsuc i) = lookup 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 (zeroβ suc (sym 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 -- Will always compute: lookup-safe : Vec A n β Fin n β A lookup-safe {A = A} xs n = Fin-elim (Ξ» {n} _ β Vec A n β A) (Ξ» {k} xs β Vec-elim (Ξ» {kβ²} _ β suc k β‘ kβ² β A) (Ξ» p β absurd (zeroβ suc (sym p))) (Ξ» x _ _ _ β x) xs refl) (Ξ» {i} j cont vec β Vec-elim (Ξ» {kβ²} xs β suc i β‘ kβ² β A) (Ξ» p β absurd (zeroβ suc (sym p))) (Ξ» {n} head tail _ si=sn β cont (Vec-cast (suc-inj (sym si=sn)) tail)) vec refl) n xs
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 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