The Church-encoded Higher-Order Free Monad for f

Free.hs

{-# LANGUAGE RankNTypes, QuantifiedConstraints, BlockArguments, LambdaCase #-}

module Free where

-- base
import Data.Coerce (coerce)


type f ~> g = forall x. f x -> g x

class (forall f. Functor f => Functor (h f)) => HFunctor h where
  hmap :: Functor f => f ~> g -> h f ~> h g

(<~$~>) :: (HFunctor h, Functor f) => f ~> g -> h f ~> h g
(<~$~>) = hmap
infixl 3 <~$~>


newtype Free h a = MkFree{
  unMkFree
    :: forall r b
    .  (a -> r b)
    -> (forall x. x -> r x)
    -> (forall x. h r (r x) -> r x)
    -> r b
} deriving Functor

instance Applicative (Free h) where
  pure x = MkFree \gen _ _ -> gen x
  liftA2 f fx fy = MkFree \gen point alg -> unMkFree fx
    (\x -> unMkFree fy
      (\y -> gen (f x y))
      point alg
    )
    point alg

instance Monad (Free h) where
  fx >>= k = MkFree \gen point alg -> unMkFree fx
    (\x -> unMkFree (k x) gen point alg)
    point alg

op :: HFunctor h => h (Free h) (Free h a) -> Free h a
op hfx = MkFree \gen point alg ->
  alg (hfold point alg <~$~> fold gen point alg <$> hfx)

fold
  :: (a -> g b)
  -> (forall x. x -> g x)
  -> (forall x. h g (g x) -> g x)
  -> Free h a -> g b
fold gen point alg fx = unMkFree fx gen point alg

hfold
  :: (forall x. x -> g x)
  -> (forall x. h g (g x) -> g x)
  -> Free h ~> g
hfold point alg fx = unMkFree fx point point alg


data (h + i) f a = InL (h f a) | InR (i f a)
  deriving Functor

instance (HFunctor h, HFunctor i) => HFunctor (h + i) where
  hmap f = \case
    InL hfx -> InL (hmap f hfx)
    InR ifx -> InR (hmap f ifx)

(<#>) :: (h f a -> g b) -> (i f a -> g b) -> (h + i) f a -> g b
left <#> right = \case
  InL hfx -> left  hfx
  InR ifx -> right ifx
infixr 6 <#>


newtype Alg sig f a = MkAlg{ unMkAlg :: sig a }
  deriving Functor

instance Functor sig => HFunctor (Alg sig) where
  hmap _ = coerce


newtype Scoped gam f a = MkScoped{ unMkScoped :: gam (f a) }
  deriving Functor

instance Functor gam => HFunctor (Scoped gam) where
  hmap f = MkScoped . fmap f . unMkScoped


newtype Prog sig gam a = MkProg{ unMkProg :: Free (Alg sig + Scoped gam) a }
  deriving (Functor, Applicative, Monad)

foldProg
  :: (Functor sig, Functor gam)
  => (a -> g b)
  -> (forall x. x -> g x)
  -> (forall x. sig (g x) -> g x)
  -> (forall x. gam (g (g x)) -> g x)
  -> Prog sig gam a -> g b
foldProg gen point alg1 alg2
  = fold gen point (alg1 . unMkAlg <#> alg2 . unMkScoped)
  . unMkProg