Boehm-Berarducci

main.hs

{-# LANGUAGE Rank2Types #-}

newtype List a = List (forall r. (a -> r -> r) -> r -> r)

instance Show a => Show (List a) where
  show (List xs) = show $ xs (:) []

nil :: List a
nil = List $ \f x -> x
cons :: a -> List a -> List a
cons b (List bs) = List $ \f x -> f b (bs f x)

data ListF a b = Cons a b | Nil

roll :: ListF a (List a) -> List a
roll (Cons b bs) = cons b bs
roll Nil = nil

unroll :: List a -> ListF a (List a)
unroll (List e) = e dCons dNil where
  dCons :: a -> ListF a (List a) -> ListF a (List a)
  dCons b bs = Cons b (roll bs)
  dNil :: ListF a (List a)
  dNil = Nil

newtype ListD a = ListD {unListD :: forall w. (a -> List a -> w) -> w -> w}

decon :: List a -> ListD a
decon (List e) = e dCons dNil where
  dCons :: a -> ListD a -> ListD a
  dCons b (ListD bs) = ListD $ \c n -> c b (bs cons nil)
  dNil :: ListD a
  dNil = ListD $ \c n -> n

head1 :: List a -> Maybe a
head1 xs = let ListD d = decon xs in d (\b bs -> Just b) Nothing 
tail1 :: List a -> Maybe (List a)
tail1 xs = let ListD d = decon xs in d (\b bs -> Just bs) Nothing

head2 :: List a -> Maybe a
head2 (List xs) = unListD (xs (\b (ListD bs) -> ListD $ \c n -> c b (bs cons nil)) (ListD $ \c n -> n)) (\b bs -> Just b) Nothing
tail2 :: List a -> Maybe (List a)
tail2 (List xs) = unListD (xs (\b (ListD bs) -> ListD $ \c n -> c b (bs cons nil)) (ListD $ \c n -> n)) (\b bs -> Just bs) Nothing

-- tail = \s. s (\b bs. \c n -> c b (bs (\b bs. \f x. f b (bs f x)) (\f x. x))) (\c n -> n) (\b bs -> Just bs) Nothing