data Void
void :: Void -> a
-- illogically, Haskell rejects the empty case distinction
void _ = error "I will never be here"
instance Show Void where
show x = void x
instance Eq Void where
x == y = void x
data CList a = Var a
| Nil
| RCons Int (CList (Maybe a)) deriving (Show, Eq)
instance Functor CList where
fmap f (Var a) = Var (f a)
fmap f Nil = Nil
fmap f (RCons x xs) = RCons x (fmap (fmap f) xs)
clist1 = RCons 1 (RCons 2 (Var Nothing))
clist2 = RCons 1 (RCons 2 (RCons 3 (Var (Just Nothing))))
ccons :: Int -> CList Void -> CList Void
ccons x xs = RCons x (shift xs)
shift :: CList a -> CList (Maybe a)
shift (Var z) = Var (Just z)
shift Nil = Nil
shift (RCons x xs) = RCons x (shift xs)
chead :: CList Void -> Int
chead (Var z) = void z
chead (RCons x _) = x
ctail :: CList Void -> CList Void
ctail (Var z) = void z
ctail (RCons x xs) = csnoc x xs
csnoc :: Int -> CList (Maybe a) -> CList a
csnoc y (Var Nothing) = RCons y (Var Nothing)
csnoc y (Var (Just z)) = Var z
csnoc y Nil = Nil
csnoc y (RCons x xs) = RCons x (csnoc y xs)
unwind :: CList Void -> [Int]
unwind Nil = []
unwind xs = chead xs : unwind (ctail xs)
cheadtail :: CList Void -> Maybe (Int, CList Void)
cheadtail Nil = Nothing
cheadtail xs = Just (chead xs, ctail xs)
cunfoldLA :: Eq c => (c -> Maybe (Int, c)) -> c -> CList Void
cunfoldLA = cunfoldLA' [] []
cunfoldLA' :: Eq c => [c] -> [a]
-> (c -> Maybe (Int, c)) -> c -> CList a
cunfoldLA' cs as ht c = case lookup c (zip cs as) of
Nothing -> case ht c of
Nothing -> Nil
Just (x, c') -> let cs' = cs ++ [c]
as' = Nothing : map Just as
in RCons x (cunfoldLA' cs' as' ht c')
Just a -> Var a
czipWith :: (Int -> Int -> Int)
-> CList Void -> CList Void -> CList Void
czipWith f xs ys = cunfoldLA ht (xs, ys) where
ht (xs, ys) = case cheadtail xs of
Nothing -> Nothing
Just (x, xs') -> case cheadtail ys of
Nothing -> Nothing
Just (y, ys') -> Just (f x y, (xs',ys'))
cfold :: (forall a . a -> g a)
-> (forall a . g a)
-> (forall a . Int -> g (Maybe a) -> g a)
-> CList a -> g a
cfold v n r (Var z) = v z
cfold v n r Nil = n
cfold v n r (RCons x xs) = r x (cfold v n r xs)
{-
newtype CListMaybe a = CLM {unCLM :: CList (Maybe a) }
shift :: CList a -> CList (Maybe a)
shift = unCLM . cfold v n r where
v z = CLM (Var (Just z))
n = CLM Nil
r x ys = CLM (RCons x (unCLM ys))
-}
cefold :: (forall a. Maybe (h a) -> h (Maybe a))
-> (forall a . h a -> g a)
-> (forall a . g a)
-> (forall a . Int -> g (Maybe a) -> g a)
-> CList (h a) -> g a
cefold d v n r (Var z) = v z
cefold d v n r Nil = n
cefold d v n r (RCons x xs) = r x (cefold d v n r (fmap d xs))
{-
csnoc :: Int -> CList (Maybe a) -> CList a
csnoc y = cefold id v n r where
v Nothing = RCons y (Var Nothing)
v (Just z) = Var z
n = Nil
r x ys = RCons x ys
-}
cunfold ::
(forall a. g a -> Either a (Maybe (Int, g (Maybe a))))
-> g a -> CList a
cunfold lht c = case lht c of
Left z -> Var z
Right Nothing -> Nil
Right (Just (x, c')) -> RCons x (cunfold lht c')
---
data CTree a = VarT a
| Leaf
| RBin Int (CTree (Maybe a)) (CTree (Maybe a))
ctree = RBin 1 (RBin 2 (RBin 3 (VarT Nothing) Leaf)
Leaf)
(RBin 4 (RBin 5 Leaf Leaf)
(RBin 6 Leaf Leaf))
cbin :: Int -> CTree Void -> CTree Void -> CTree Void
cbin x xsL xsR = RBin x (shiftT xsL) (shiftT xsR)
shiftT :: CTree a -> CTree (Maybe a)
shiftT (VarT x) = VarT (Just x)
shiftT Leaf = Leaf
shiftT (RBin x xsL xsR) = RBin x (shiftT xsL) (shiftT xsR)
csubL :: CTree Void -> CTree Void
csubL (VarT z) = void z
csubL (RBin x xsL xsR) = csnocL x xsR xsL
csubR :: CTree Void -> CTree Void
csubR (VarT z) = void z
csubR (RBin x xsL xsR) = csnocR x xsL xsR
csnocL :: Int -> CTree (Maybe a) -> CTree (Maybe a) -> CTree a
csnocL y ys (VarT Nothing) = RBin y (VarT Nothing) ys
csnocL y ys (VarT (Just z)) = VarT z
csnocL y ys Leaf = Leaf
csnocL y ys (RBin x xsL xsR) = RBin y (csnocL y ys' xsL)
(csnocL y ys' xsR)
where ys' = shiftT ys
csnocR :: Int -> CTree (Maybe a) -> CTree (Maybe a) -> CTree a
csnocR y ys (VarT Nothing) = RBin y ys (VarT Nothing)
csnocR y ys (VarT (Just z)) = VarT z
csnocR y ys Leaf = Leaf
csnocR y ys (RBin x xsL xsR) = RBin x (csnocR y ys' xsL)
(csnocR y ys' xsR)
where ys' = shiftT ys