Freer.hs

{-# LANGUAGE Arrows                 #-}
{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE NoImplicitPrelude      #-}
{-# LANGUAGE OverlappingInstances   #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE Rank2Types             #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}

module Control.Arrow.Free
  ( Freer(..)
  ) where

import Control.Arrow
import Control.Category
import Data.Proxy
import Data.Constraint  ((:-)(Sub), Dict(Dict))
import Data.Function    (const, ($))

type x ~> y = forall a b. x a b -> y a b

newtype Freer cst eff a b = Freer {
  runFreer :: forall x. cst x => (eff ~> x) -> x a b
}

class Class1 b  h | h -> b where
  cls1 :: h a :- b a

instance Class1 Category Arrow where cls1 = Sub Dict
instance Class1 Category ArrowChoice where cls1 = Sub Dict

cls1WithType :: Class1 b h => Proxy h -> Proxy b -> (eff ~> x) -> h x :- b x
cls1WithType _ _ _ = cls1

instance Category (Freer Category eff) where
  id = Freer $ const id
  Freer f . Freer g = Freer $ \x -> f x . g x
instance (Class1 Category c) => Category (Freer c eff) where
  id = Freer $ \g -> case cls1WithType (Proxy :: Proxy c) (Proxy :: Proxy Category) g of
    Sub Dict -> id
  Freer f . Freer g = Freer $ \x -> case cls1WithType (Proxy :: Proxy c) (Proxy :: Proxy Category) x of
    Sub Dict -> f x . g x

test :: Freer Arrow eff a a
test = id