type Zero {[ * ]} t1 = t1
type Zero {[k -> l]} t1 = forall a. Zero {[k]} a -> Zero{[ l]} (t1 a)

zero {| t :: k |} :: Zero {[ k ]} t
zero {| Unit |} = ()
zero {| Int  |} = 0
zero {| Char |} = '0'
zero {| :+:  |} zA zB = Inl zA
zero {| :*:  |} zA zB = (zA, zB)
zero {| (->) |} zA zB = \x -> zB

zero {| List |} :: forall a. a -> List a

  

















--- Eq 
type Peq {[ * ]} t = t -> t -> Bool
type Peq {[ k -> l ]} t = forall a. Peq {[k]} a -> Peq {[ l ]} (t a)

peq {| t :: k |} :: Peq {[ k ]} t
peq {| Unit |} x y = True 
peq {| :+: |}   peqA peqB (Inl x) (Inl y)   =  peqA x y
peq {| :+: |}  peqA peqB (Inr x) (Inr y)     =  peqB x y
peq {| :+: |}  _       _         peqA peqB  = False
peq {| :*: |}  (x1 :*: y1)  (x2 :*: y2) peqA peqB  = peqA x1 x2 && peqB y1 y2 
peq {| Int |}     = (==)
peq {| Integer |} = (==)
peq {| Float |}   = (==)
peq {| Double |}  = (==)
peq {| Char |}    = (==)
peq {| Bool |}    = (==)

--- Size

type Size {[ * ]} t = t -> Int
type Size {[ k -> l ]} t = forall a. Size {[k]} a -> Size {[l]} (t a)
size {| t :: k |} :: Size {[ k ]} t b
size {| Unit |}      x             =  0
size {| :+: |}  (Inl x)   szA szB  =  szA x
size {| :+: |}  (Inr y)   szA szB  =  szB y
size {| :*: |}  (x :*: y) szA szB  =  (szA x) + (szB y)
size {| Int |}       x             =  0
size {| Integer |}   x             =  0
size {| Float |}     x             =  0
size {| Double |}    x             =  0
size {| Char |}      x             =  0
size {| Bool |}      x             =  0


type Size {[ * -> * ]} t = forall a. (a -> Int) -> t a -> Int

type Maybe = \a:*. Unit :+: a

f :: Maybe a -> Int
f = size {|Maybe|} (\x -> 1)

type List = \a:*. Fix (\b:*. Unit :+: (a :*: b))

f :: List a -> Int
f = size {|List|} (\x -> 1)











--- Reductions  (like folds)

type Rreduce {[ * ]} t b = t -> b -> b
type Rreduce {[ k -> l ]} t b = forall a. Rreduce{[ k]} a b -> Rreduce {[ l ]} (t a) b

rreduce {| t :: k |} :: Rreduce {[ k ]} t b
rreduce {| Unit |}      x          e  =  e
rreduce {| :+: |}  (Inl x)   rrA rrB e  =  rrA e
rreduce {| :+: |}  (Inr y)   rrA rrB e  =  rrB e
rreduce {| :*: |}  (x :*: y) rrA rrB e  =  rrA x (rrB y e)
rreduce {| Int |}       x          e  =  e
rreduce {| Integer |}   x          e  =  e
rreduce {| Float |}     x          e  =  e
rreduce {| Double |}    x          e  =  e
rreduce {| Char |}      x          e  =  e
rreduce {| Bool |}      x          e  =  e


type Lreduce{[ * ]} t b = b -> t -> b
type Lreduce{[ k -> l ]} t b = forall a. Lreduce{[ k]} a b -> Lreduce {[ l ]} (t a) b

lreduce {| t :: k |} ::  Lreduce {[ k ]} t b
lreduce {| Unit |}     e  x          =  e
lreduce {| :+: |}  e  (Inl x)  lrA lrB  =  lrA e x
lreduce {| :+: |}  e  (Inr y)  lrA lrB  =  lrB e y
lreduce {| :*: |}  e  (x :*: y) lrA lrB  =  lrB (lrA e x) y
lreduce {| Int |}      e  x          =  e
lreduce {| Integer |}  e  x          =  e
lreduce {| Float |}    e  x          =  e
lreduce {| Double |}   e  x          =  e
lreduce {| Char |}     e  x          =  e
lreduce {| Bool |}     e  x          =  e

-- specializations  
crush {| t :: * -> *  |} ::  (a -> a -> a) -> a -> t a -> a
crush {| t |} op e xs = lreduce {| t |} op e xs

gsum {| t :: * -> *  |} :: (Num a) => t a -> a
gsum {| t |} xs = lreduce {| t |} (+) 0 xs

gproduct {| t :: * -> * |} :: (Num a) => t a -> a
gproduct {| t |} xs = lreduce {| t |} (*) 1 xs

gand {| t :: * -> * |} ::  t Bool -> Bool
gand {| t |} xs = lreduce {| t |} (&&) True xs

gor {| t :: * -> * |} ::  t Bool -> Bool
gor {| t |} xs = lreduce {| t |} (||) False xs

flatten {| t :: * -> * |} ::  t a -> [a]
flatten {| t |} xs = rreduce {| t |} (:) xs []

count {| t :: * -> * |} ::  t a -> Int
count {| t |} xs = rreduce {| t |} (const (+1)) xs 0

comp {| t :: * -> *  |} ::  t (a -> a) -> (a -> a)
comp {| t |} xs = lreduce {| t |} (.) id xs

gconcat {| t :: * -> * |} ::  t [a] -> [a]
gconcat {| t |} xs = lreduce {| t |} (++) [] xs

gall {| t :: * -> * |} :: (a -> Bool) -> t a -> Bool
gall {| t |} p xs = lreduce {| t |} (\a b -> a && p b) True xs 

gany {| t :: * -> * |} :: (a -> Bool) -> t a -> Bool
gany {| t |} p xs = rreduce {| t |} (\a b -> p a || b) xs False

gelem {| t :: * -> * |} :: a -> t a -> Bool
gelem {| t |} x xs = rreduce {| t |} (\a b -> a == x || b) xs False

-- printing types 

type Pt {[*]} a = String
type Pt {[k -> l]} b = forall a. Pt {[k]} a -> Pt {[l]} (t a)
pt {| t :: k |} :: Pt {[ k ]} t

pt {| Unit |} = "Unit"
pt {| Int  |} = "Int"
pt {| Char |} = "Char"
pt {| :+:  |} zA zB = "(" ++ zA ++ ":+:" ++ zB ")"
pt {| :*:  |} zA zB = "(" ++ zA ++ ":*:" ++ zB ")"
pt {| (->) |} zA zB = "(" ++ zA ++ "->" ++ zB ")"













{-
type Pt {[*]} = String
type Pt {[k -> l]} = Pt {[k]} -> Pt {[l]}
pt {| t :: k |} :: Pt {[ k ]} 

pt {| Unit |} = "Unit"
pt {| Int  |} = "Int"
pt {| Char |} = "Char"
pt {| :+:  |} zA zB = "(" ++ zA ++ ":+:" ++ zB ")"
pt {| :*:  |} zA zB = "(" ++ zA ++ ":*:" ++ zB ")"
pt {| (->) |} zA zB = "(" ++ zA ++ "->" ++ zB ")"
-}

--- Mapping


type Map {[ * ]} t1 f = t1 -> (f t1)
type Map {[ k -> l ]} t1 f = forall u1 g::* ->&.
  Map {[ k ]} u1 g -> Map {[ l ]} (t1 u1) (t1 u1)


type Map {[ * ]} t1 t2 = t1 -> t2 
type Map {[ k -> l ]} t1 t2 = forall u1 u2.
  Map {[ k ]} u1 u2 -> Map {[ l ]} (t1 u1) (t2 u2)

gmap {| t :: k |} :: Map {[ k ]} t t 
-- gmap {| Unit |}     = id
gmap {| :+: |}     gmapA gmapB (Inl a)     = Inl (gmapA a)
gmap {| :+: |}     gmapA gmapB (Inr b)     = Inr (gmapB b)
gmap {| :*: |}     gmapA gmapB (a :*: b)   = (gmapA a) :*: (gmapB b)
gmap {| (->) |}    gmapA gmapB _           = error "gmap not defined for function types"
gmap {| Con c |}   gmapA       (Con a)     = Con (gmapA a)
gmap {| Label l |} gmapA       (Label a)   = Label (gmapA a)
-- gmap {| Int |}      = id
-- gmap {| Char |}     = id 
-- gmap {| Bool |}     = id
gmap {| :: * |}        = id
gmap {| IO |} gmapA = fmap gmapA  
gmap {| [] |} gmapA = map gmapA

data List a = Nil | Cons a (List a) deriving Show
data Tree a b = Leaf a | Bin (Tree a b) b (Tree a b) deriving Show

exTree :: Tree Int Int
exTree = Bin (Bin (Leaf 1) 2 (Leaf 3)) 4 (Leaf 5)

mapList = gmap {| List |}
mapTree = gmap {| Tree Int |}