Possibly pointless? encoding of lists as their own paramorphisms.

para.hs

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE Rank2Types #-}

import Data.Maybe

data Fix f = Fix { unFix :: f (Fix f) }

data ListF a b = LF { unLF :: forall c. (Maybe (a, (c, b)) -> c) -> c }

type List a = Fix (ListF a)

wrap :: (forall c. (Maybe (a, (c, List a)) -> c) -> c) -> List a
wrap f = Fix (LF f)

unwrap :: List a -> (forall c. (Maybe (a, (c, List a)) -> c) -> c)
unwrap = unLF . unFix

nil :: List a
nil = wrap (\f -> f Nothing)

cons :: a -> List a -> List a
cons x xs = wrap (\f -> f (Just (x, (unwrap xs f, xs))))

cata :: List a -> (Maybe (a, b) -> b) -> b
cata xs f = unwrap xs (f Nothing `maybe` uncurry (\x -> uncurry (\r _ -> f (Just (x, r)))))

para :: List a -> (Maybe (a, (b, List a)) -> b) -> b
para = unwrap

elim :: List a -> (Maybe (a, List a) -> b) -> b
elim xs f = unwrap xs (f Nothing `maybe` uncurry (\x -> uncurry (\_ xs -> f (Just (x, xs)))))

isEmpty :: List a -> Bool
isEmpty xs = elim xs (True `maybe` \_ -> False)

hd :: List a -> Maybe a
hd xs = elim xs (Nothing `maybe` (Just . fst))

tl :: List a -> Maybe (List a)
tl xs = elim xs (Nothing `maybe` (Just . snd))

len :: (Num b, Enum b) => List a -> b
len xs = cata xs (0 `maybe` uncurry (const succ))

xs = cons 1 (cons 2 (cons 3 nil))