Para.idr

%default total

data Mu : (Type -> Type) -> Type where
    In : f (Mu f) -> Mu f

out : Mu f -> f (Mu f)
out (In x) = x

data LstF : Type -> Type -> Type where
    LF : ({c : Type} -> (Maybe (a, Unit -> c, b) -> c) -> c) -> LstF a b

unLF : LstF a b -> ({c : Type} -> (Maybe (a, Unit -> c, b) -> c) -> c)
unLF (LF x) = x

Lst : Type -> Type
Lst a = Mu (LstF a)

wrap : ({c : Type} -> (Maybe (a, Unit -> c, Lst a) -> c) -> c) -> Lst a
wrap = In . LF

unwrap : Lst a -> ({c : Type} -> (Maybe (a, Unit -> c, Lst a) -> c) -> c)
unwrap = unLF . out

nil : Lst a
nil = wrap (\f => f Nothing)

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

strictMaybe : b -> (a -> b) -> Maybe a -> b
strictMaybe x _ Nothing = x
strictMaybe _ f (Just x) = f x

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

lazyCata : (Maybe (a, Unit -> b) -> b) -> Lst a -> b
lazyCata f xs = unwrap xs ((\_ => f Nothing) `strictMaybe` uncurry (\x => uncurry (\r, _, _ => f (Just (x, r ()))))) ()

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

isEmpty : Lst a -> Bool
isEmpty xs = elim xs (True `strictMaybe` const False)

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

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

xs : Lst Nat
xs = cons 1 (cons 2 (cons 3 nil))