List Codensity transformation in Idris

Codensity.idr

module Main

data Free : (f : Type -> Type) -> (a : Type) -> Type where
  Pure : a -> Free f a
  Bind : f (Free f a) -> Free f a

instance Functor f => Functor (Free f) where
  map f (Pure x) = Pure (f x)
  map f (Bind x) = assert_total (Bind (map (map f) x))

instance Functor f => Applicative (Free f) where
  pure = Pure

  (Pure f) <*> x = map f x
  (Bind f) <*> x = assert_total (Bind (map (<*> x) f))

instance Functor f => Monad (Free f) where
  (Pure x) >>= f = f x
  (Bind x) >>= f = assert_total (Bind (map (>>= f) x))

instance Functor (Pair a) where
  map f (x, y) = (x, f y)

(>>) : Monad m => m a -> m b -> m b
x >> y = x >>= \_ => y

liftFree : Functor f => f a -> Free f a
liftFree = Bind . map Pure

data Codensity : (m : Type -> Type) -> (a : Type) -> Type where
  Codense : ({b : Type} -> (a -> m b) -> m b) -> Codensity m a

runCodensity : Codensity m a -> ({b : Type} -> (a -> m b) -> m b)
runCodensity (Codense c) = c

instance Functor (Codensity f) where
  map f (Codense c) = Codense (\k => c (k . f))

instance Applicative (Codensity f) where
  pure x = Codense (\k => k x)
  (Codense f) <*> (Codense x) = Codense (\k => x (\x' => f (\f' => k (f' x'))))

instance Monad (Codensity f) where
  (Codense x) >>= f = Codense (\k => x (\x' => runCodensity (f x') k))

liftCodensity : Monad m => m a -> Codensity m a
liftCodensity x = Codense (x >>=)

lowerCodensity : Monad m => Codensity m a -> m a
lowerCodensity (Codense c) = c return

exec : Free (Pair a) () -> List a
exec (Pure _)       = []
exec (Bind (x, xs)) = x :: exec xs

DList : Type -> Type
DList a = Codensity (Free (Pair a)) ()

empty : DList a
empty = liftCodensity (Pure ())

singleton : a -> DList a
singleton x = liftCodensity (liftFree (x, ()))

toList : DList a -> List a
toList = exec . lowerCodensity

cons : a -> DList a -> DList a
cons x xs = singleton x >> xs

snoc : DList a -> a -> DList a
snoc xs x = xs >> singleton x

(++) : DList a -> DList a -> DList a
xs ++ ys = xs >> ys

test : Maybe Int
test = last' (toList (foldl snoc empty [1..10000]))

main : IO ()
main = print test