module L3 where ---------------------------------------------------------------------- -- Lecture 3 : Vectors and Finite Sets -- ---------------------------------------------------------------------- data Nat : Set where zero : Nat suc : Nat -> Nat data _^_ (X : Set) : Nat -> Set where [] : X ^ zero _::_ : {n : Nat} -> X -> X ^ n -> X ^ suc n {- Finite sets describe positions in vectors: no positions in [] a head position and some tail positions for _::_ -} data Fin : Nat -> Set where fzero : {n : Nat} -> Fin (suc n) fsuc : {n : Nat} -> Fin n -> Fin (suc n) vec : {n : Nat}{X : Set} -> X -> X ^ n vec {zero} x = [] vec {suc n} x = x :: vec {n} x _$s_ : {n : Nat}{S T : Set} -> (S -> T) ^ n -> S ^ n -> T ^ n [] $s [] = [] (f :: fs) $s (s :: ss) = f s :: (fs $s ss) infixl 90 _$s_ proj : {n : Nat}{X : Set} -> X ^ n -> Fin n -> X proj [] () proj (x :: xs) fzero = x proj (x :: xs) (fsuc i) = proj xs i tabulate : {n : Nat}{X : Set} -> (Fin n -> X) -> X ^ n tabulate {zero} f = [] tabulate {suc n} f = f fzero :: tabulate (\ i -> f ( fsuc i ) ) positions : {n : Nat} -> Fin n ^ n positions = tabulate (\ p -> p ) tabulate' : {n : Nat}{X : Set} -> (Fin n -> X) -> X ^ n tabulate' f = vec f $s positions