Implementing algebraic effects through typeclass prolog

We will be writing a lot of type level code and consequently, we will need to give the compiler a a lot of LANGUAGE pragmas.

To be able to construct a [* -> *]:

{-# LANGUAGE DataKinds #-}

To be able to express that every element of a [* -> *] is a functor:

{-# LANGUAGE TypeFamilies #-}

For more complex instance declarations:

{-# LANGUAGE UndecidableInstances #-}

To be able to express PreservesShow:

{-# LANGUAGE QuantifiedConstraints #-}

To disambiguate some types:

{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}

Some of the type families we are going to define are actually constraints.

import GHC.Exts (Constraint)

One of the ideas explained in the paper [1] is that we can create an extensible syntax tree by representing each constructor with a functor, by combining constructors with sums of functors and by making this type recusive through the fixpoint operator for functors.

The fixpoint operator and an example of a constructor we might want to add to a syntax tree:

data Fix f = In (f (Fix f))

data Plus s = -- s for self. This is the point of recursion
  Plus s s
  deriving (Functor, Show)

We will reuse the idea of sums of functors to represent different effects (each functor is responsible for an effect), but instead of making the tree recursive through the fixpoint operator, we will take the free monad from the sum of functors.

The free monad Free f makes f into a monad, because a term of type Free f x is inhabited by terms of shape for some . is Return and the Join operation works becaus .

data Free f x = Return x | Join (f (Free f x))
  deriving Functor

If we have a list of effects fs :: [* -> *], we would like to have a way to combine these into a new functor * -> *. This is what this type does.

data Sum (fs :: [* -> *]) (x :: *) where
  Head :: f x -> Sum (f ': fs) x
  Tail :: Sum fs x -> Sum  (f ': fs) x

A term of type Sum '[A, B, C] x is either a term of type A x, B x or C x.

For type inference to work well for us, we want our "effect sets" relations to be computed by Haskell's instance resolution system. We will define a typeclass for every relation we wish to have on effect sets. We will then define instances (derivation rules) through with the Haskell compiler will generate code for us.

We first need an "is-element" relation(it is very similar to the typeclass they use in [1]) which will be witnessed by a way to turn an f x into a Sum fs x whenever f :∈: fs.

class (e :: * -> *) :∈: (es :: [* -> *]) where
  inject :: e x -> Sum es x

To make the compiler automatically verify this relation, we will give it derivation rules:

An effect is an element of an effect set if it is the first element of the set.

instance {-# OVERLAPPING #-} f :∈: (f ': fs) where
  inject = Head

An effect is also an element of an effect set if it is an element of the tail of the set.

instance f :∈: fs => f :∈: (g':fs) where
  inject = Tail . inject

Here is an example of this typeclass in action. We use it to automatically "cast" a term to a "bigger" type.

data A s = A s
data B s = B s

test1 :: Sum '[A, B] Int
test1 = inject $ B 12

With the help of our membership relation, we can define a new relation which will let us express the fact an effect set is smaller than an other effect set. This relation will be witnessed by a function very similar to inject, apart for the fact it converts from a Sum.

class (l :: [* -> *]) :⊆: (r :: [* -> *]) where
  permute :: Sum l x -> Sum r x

The empty set is a subset of everything (this is the base case of our typeclass recursion).

instance '[] :⊆: fs where
  -- no constructors for Sum '[] x
  permute _ = error "impossible"

If the first element of the LHS set is a member of the RHS set and the last elements of the LHS set are a subset of the RHS, then the LHS is a subset of the RHS. (this is the induction case of our typeclass recursion)

instance (f :∈: gs, fs :⊆: gs) => (f ': fs) :⊆: gs where
  permute (Head h) = inject h
  permute (Tail t) = permute t

Here is an example of ho we might use this relation:

data C s = C s

test2 :: Sum '[B, C, A] Int
test2 = permute test1

Because of the way we set up our derivation rules, whenever all the functors in a set are known, the instance search algorithm will automatically generate the necessary code to rearange the order of a functor sum.

Now we ave a way to represent effects (as sum of functors), let's tie them in a circle using the free monad. The following construction is equivalent to the free monad on the sum of the effects.

data Eff (fs :: [* -> *]) (x :: *) where
  Pure :: x -> Eff fs x
  Impure :: Sum fs (Eff fs x) -> Eff fs x

-- To unwrapp empty effects into pure values
unwrapEff :: Eff '[] x -> x
unwrapEff (Impure _) = error "impossible"
unwrapEff (Pure x) = x

This construction will let us sequence many effects together. Another thing to notice is that

We all know the meme phrase "a monad is just a monoid in the category of endofunctors", but what does it tell us about the free monad? It is just the free monoid in the category of endofunctors.

When working with effectful values, it will be useful to have Show (Eff fs x) when possible. To achieve this, we will need to define new typeclasses and some instances.

We say that a * -> * "preserves show" when Show (f x) whenever Show x.

class (forall x. Show x => Show (f x)) => PreservesShow f

We know that Sum fs preserves show if and only if al of the elements of fs preserve it too.

type family AllPreserveShow (fs :: [* -> *]) :: Constraint where
  AllPreserveShow (f ': fs) = (PreservesShow f, AllPreserveShow fs)
  AllPreserveShow '[] = ()

instance (AllPreserveShow fs, Show x) => Show (Sum fs x) where
  show (Head h) = show h
  show (Tail t) = show t

Finally, because Eff fs x uses Sum fs, it also preserves show whenever Sum fs preserves show.

instance (AllPreserveShow fs, Show x) => Show (Eff fs x) where
  show (Pure x) = show x
  show (Impure t) = show t

Further down, having Functor instances for everything will be very useful. This is why it is important automatically derive Functor instances whenever possible.

type family AllFunctors (fs :: [* -> *]) :: Constraint where
  AllFunctors (f ': fs) = (Functor f, AllFunctors fs)
  AllFunctors '[] = ()

Again, a sum of * -> *s is a functor if and only if they all are.

instance AllFunctors fs => Functor (Sum fs) where
  fmap f (Head h) = Head $ fmap f h
  fmap f (Tail t) = Tail $ fmap f t

By the same reasoning as with Show, Eff fs is a functor whenever fs are.

instance AllFunctors fs => Functor (Eff fs) where
  fmap f (Pure x) = Pure $ f x
  fmap f (Impure fx) = Impure $ (fmap . fmap) f fx

The categorical presentation of a monad uses a join operator instead of >>=. Here, we will first implement effJoin (it simply removes a Pure between the two layers of Eff fs) and derive effBind with it.

effJoin :: AllFunctors fs => Eff fs (Eff fs x) -> Eff fs x
effJoin (Pure x) = x
effJoin (Impure fx) = Impure $ (fmap effJoin) fx

effBind :: AllFunctors fs => Eff fs x -> (x -> Eff fs y) -> Eff fs y
effBind fx f = effJoin $ fmap f fx

The two instances we need to have Monad (Eff fs) then flow naturally.

instance (AllFunctors fs) => Applicative (Eff fs) where
  pure = Pure
  ff <*> fx = effBind ff (\f -> fmap f fx)

instance (AllFunctors fs) => Monad (Eff fs) where
  (>>=) = effBind

I hear you ask: "At the beginning, you presented algebraic effects as an alternative to monads, so why are you making Eff fs a monad?"

The reason algebraic effects are interesting is because they compose very well. Monads, in their normal form, don't. What we do here is compose the effects before turning them into a monad. This way, we only have to think about a single "monad constructor": Eff.

Now that we have built ourselves an ontology of typeclasses, functors and monads, we need utilities to actually use the algebraic effects. The first one of them will be this simple effInj function which will let us turn a naked effect into a fully-clothed effectful value.

effInj :: (Functor f, f :∈: fs) => f x -> Eff fs x
effInj e = Impure $ inject $ fmap Pure e

Here is how to use it. Let's say we defined two effects for asking for a string and asking for an integer. The function that will find itself inside the GetInt or the GetString will be the continuation (you can read more about continuations in My last post) to which will be passed the String or Int. Here, we use id, because the continuation of our block will automatically be add through the monadic operations.

data GetString a = GetString (String -> a)
  deriving Functor

data GetInt a = GetInt (Int -> a)
  deriving Functor

type MyEff = [GetString, GetInt]

comp :: Eff MyEff String
comp = do
  int <- effInj $ GetInt id
  str <- effInj $ GetString id
  return $ str ++ show int

Here is an utility function to embed an effectful value into a bigger effect space.

effPerm :: forall fs gs x. (AllFunctors fs, fs :⊆: gs) => Eff fs x -> Eff gs x
effPerm (Pure x) = Pure x
effPerm (Impure sx) = Impure $ permute @fs @gs $ fmap (effPerm @fs @gs) sx

The idea of a handler is what makes algebraic effects ergonomic. It lets us easily handle one of the effects using the other effects in the set.

handle :: forall fs g gs x. (Functor g, AllFunctors gs, AllFunctors fs,fs :⊆: (g ': gs))
  => (forall x. g x -> Eff gs x) -> Eff fs x -> Eff gs x
handle trans (Pure x) = (Pure x)
handle trans (Impure x) = case permute @fs @(g ': gs) x of
  Head h -> let val = fmap (handle trans) h
                val' = trans val
            in effJoin val'
  Tail t -> let val = fmap (handle @fs @g @gs trans) t
            in Impure val

You use handle a bit like you use try / catch blocks in other programming languages. Whenever the effect you want to eliminate is used, you must do so using one of the remaining effects in the set.

comp' :: Eff '[GetString] String
comp' = handle func comp
  where func :: GetInt x -> Eff '[GetString] x
        func (GetInt f) = return $ f 0

Let's say you want an effect GenSym :: (Int -> x) -> GenSym x that generates unique integers. We need some kind of way to remember the last number we gave out. A Handler f fs lets us handle a f effect using fs and also, at the same time, give the next Handler f fs to use.

data Handler (f :: * -> *) (fs :: [* -> *]) where
  Handler :: (forall x. f x -> Eff fs (x, Handler f fs)) -> Handler f fs

Now we need a handleFold function.

handleFold :: forall fs g gs x. (Functor g, AllFunctors gs, AllFunctors fs,fs :⊆: (g ': gs))
  => Handler g gs -> Eff fs x -> Eff gs x
handleFold _ (Pure x) = Pure x
handleFold (Handler fold) (Impure x) = case permute @fs @(g ': gs) x of
  Tail t -> Impure $ fmap (handleFold (Handler fold)) t
  Head h -> do
    (val, fold') <- fold h
    handleFold fold' val

Example:

data GenSym x = GenSym (Int -> x)
  deriving Functor

syms :: Eff '[GenSym] [Int]
syms = do
  x <- effInj $ GenSym id
  y <- effInj $ GenSym id
  z <- effInj $ GenSym id
  return [x, y, z+1]

symsEvaled :: Eff '[] [Int]
symsEvaled = handleFold (fh 0) syms
  where fh :: Int -> Handler GenSym '[]
        fh k = Handler $ \(GenSym cont) -> return $ (cont k, fh (k+1))