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