module L2 where data Nat : Set where zero : Nat suc : Nat -> Nat {- Any connection between List and Nat ? -} data _^_ (X : Set) : Nat -> Set where [] : X ^ zero _::_ : {n : Nat} -> X -> X ^ n -> X ^ suc n data _*_ (S T : Set) : Set where _,_ : S -> T -> S * T zip : {n : Nat}{S T : Set} -> S ^ n -> T ^ n -> (S * T) ^ n zip [] ts = [] zip (s :: ss) (t :: ts) = (s , t ) :: zip ss ts map : {S T : Set}{n : Nat} -> (S -> T) -> S ^ n -> T ^ n map f [] = [] map f (x :: xs) = f x :: map f xs _+_ : Nat -> Nat -> Nat zero + y = y suc x + y = suc (x + y) moo : {n : Nat} -> Nat ^ n -> (Nat * Nat) ^ n moo ns = zip ns (map (\ x -> x + x) ns) foldl : {S : Set}{T : Nat -> Set} -> ({n : Nat} -> T n -> S -> T (suc n)) -> T zero -> {n : Nat} -> S ^ n -> T n foldl {T = T0} f t [] = t foldl {T = Tsn} f t (s :: ss) = foldl {T = \ n -> Tsn (suc n) } f (f t s) ss 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_ zip' : {n : Nat}{S T : Set} -> S ^ n -> T ^ n -> (S * T) ^ n zip' ss ts = vec _,_ \$s ss \$s ts map' : {n : Nat}{S T : Set} -> (S -> T) -> S ^ n -> T ^ n map' f ss = vec f \$s ss