open import 1Lab.Path
open import 1Lab.Type

open import Data.Product.NAry
open import Data.Fin.Base
open import Data.Nat.Base

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 Fin(n)β†’A\mathrm{Fin}(n) \to A, i.e., the functions from the with nn elements to the type AA. 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

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