{-# LANGUAGE ConstraintKinds, RankNTypes, MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
import Control.Monad
class Algebra f a where
phi :: f a -> a
newtype Initial p a = Initial { runInitial :: forall x. p x => (a -> x) -> x }
newtype HInitial p f a = HInitial { runHInitial :: forall m. p m => (forall x. f x -> m x) -> m a }
type FreeM f = Initial (Algebra f)
type HFreeM = HInitial Monad
instance Monad (Initial p) where
return x = Initial ($ x)
Initial m >>= f = Initial $ \k -> m (\a -> runInitial (f a) k)
liftFree :: Functor f => f a -> FreeM f a
liftFree fa = Initial $ \k -> phi (fmap k fa)
iso1 :: Functor f => HInitial Monad f a -> FreeM f a
iso1 m = runHInitial m liftFree
instance Functor f => Algebra f (HInitial Monad f a) where
phi x = HInitial $ \k -> join $ k (fmap (\x -> runHInitial x k) x)
instance Monad (HInitial Monad f) where
return a = HInitial $ \ _ -> return a
m >>= f = HInitial $ \ k -> runHInitial m k >>= (\a -> runHInitial (f a) k)
iso2 :: Functor f => FreeM f a -> HInitial Monad f a
iso2 m = runInitial m return