More GADT nonsense

{-# LANGUAGE GADTs #-}

data CON f a fa k z where
 CTR :: c -> CON f a c z z
 VAR :: CON f a (a -> r) k z -> CON f a r (a -> k) z
 REC :: CON f a (f a -> r) k z -> CON f a r (f a -> k) z

infixr :+:
data SUM f a ka z where
 ZRO :: SUM f a (f a -> z) z
 (:+:) :: CON f a (f a) k z -> SUM f a ka z -> SUM f a (k -> ka) z


size :: kase -> SUM f a kase Integer -> f a -> Integer
size kase code = size' kase code kase code
size' :: kase -> SUM f a kase Integer -> ka -> SUM f a ka Integer -> f a -> Integer
size' kase code ka ZRO = ka
size' kase code ka (t :+: ts) = size' kase code (ka (sizeCON kase code 0 t)) ts
sizeCON :: kase -> SUM f a kase Integer -> Integer -> CON f a i0 k Integer -> k
sizeCON kase code k (CTR _) = 0 + k
sizeCON kase code k (VAR r) = \_ -> sizeCON kase code (1 + k) r
sizeCON kase code k (REC r) = \x -> sizeCON kase code (size kase code x + k) r


dfs :: kase -> SUM f a kase [a] -> f a -> [a]
dfs kase code = dfs' kase code kase code
dfs' :: kase -> SUM f a kase [a] -> ka -> SUM f a ka [a] -> f a -> [a]
dfs' kase code ka ZRO = ka
dfs' kase code ka (t :+: ts) = dfs' kase code (ka (dfsCON kase code [] t)) ts
dfsCON :: kase -> SUM f a kase [a] -> [a] -> CON f a i0 k [a] -> k
dfsCON kase code k (CTR _) = k
dfsCON kase code k (VAR r) = \a -> dfsCON kase code (a : k) r
dfsCON kase code k (REC r) = \x -> dfsCON kase code (dfs kase code x ++ k) r


data Both a = a :&: a
(&) = VAR (VAR (CTR (:&:)))
both = (&) :+: ZRO
bothCase (&) (x :&: y) = x & y
bothCaseR (&) (x :&: y) = y & x

data List a = Nil | Cons a (List a)
nil = CTR (Nil)
cons = REC (VAR (CTR (Cons)))
list = nil :+: cons :+: ZRO
listCase nil cons Nil = nil
listCase nil cons (Cons x xs) = cons x xs
listCaseR nil cons Nil = nil
listCaseR nil cons (Cons x xs) = cons xs x

data Tree a = Leaf a | Branch (Tree a) (Tree a)
leaf = VAR (CTR (Leaf))
branch = REC (REC (CTR Branch))
tree = leaf :+: branch :+: ZRO
treeCase leaf branch (Leaf a) = leaf a
treeCase leaf branch (Branch l r) = branch l r
treeCaseR leaf branch (Leaf a) = leaf a
treeCaseR leaf branch (Branch l r) = branch r l

-- > size bothCaseR both (True :&: False)
-- 2
-- > size listCaseR list (Cons 'x' (Cons 'y' (Cons 'z' Nil)))
-- 3
-- > size treeCaseR tree (Branch (Leaf ()) (Branch (Branch (Leaf ()) (Leaf ())) (Leaf ())))
-- 4
-- > dfs listCaseR list (Cons 'x' (Cons 'y' (Cons 'z' Nil)))
-- "xyz"
-- > dfs treeCaseR tree (Branch (Leaf 4) (Branch (Branch (Leaf 3) (Leaf 5)) (Leaf 7)))
-- [4,3,5,7]