Encoding Higher-Order Effects in Haskell

Introduction

Algebraic effects and handlers are a popular technique for modeling side effects. A key idea behind the technique is to define effects as interfaces of effectful operations such that we can program against these interfaces, and provide independent implementations of these interfaces later. In part one of this blog post we explained how to model algebraic effects in Haskell, using mostly well-known techniques from Data Types à la Carte.

But many higher-order effects (i.e., effects with one or more operations with one or more parameters of a computation type) cannot be represented as algebraic effects using the same techniques. We can, however, apply effect handlers inside of abstract syntax trees to emulate higher-order effect interfaces. This blog post shows how to adapt the techniques from the previous blog post to support this.

The solution we present in the blog post only emulates higher-order effect interfaces, but does not support modularly changing interface implementations without changing the programs that use them. In part three of this blog post we show how to model higher-order effects as proper interfaces of effectful operations, such that we can modularly change interface implementations, like with algebraic effects and handlers. The general solution we present in part three builds on the adapted techniques we show in this blog post.

This blog post assumes familiarity with representing algebraic effects in Haskell, following the (standard) approach described in part one of this blog post.

The focus of the blog post series is to explain how to model and implement effects in a typed and conceptually clear way. There are excellent Haskell libraries available on Hackage that provide more efficient and (for many purposes) more ergonomic implementations of algebraic effects.

Contents

The Problem with Higher-Order Effects

As summarized at the end of the previous blog post, algebraic effects and handlers lets us represent and provide implementations of many different effects and operations. However, some effects are awkward to model using algebraic effects and handlers alone. Particularly higher-order effects; that is, effects with one or more operations that have one or more parameters of a computation type. Unfortunately, such higher-order effects are common. For example, Haskell’s popular monad transformer library, mtl, contains several higher-order operations, such as the local effect of the reader monad whose interface is summarized by the following type class:

class Monad m => MonadReader r m | m -> r where
  ask   :: m r
  local :: (r -> r) -> m a -> m a
--                     ^^^ computation typed parameter

As explained in the previous blog post, an algebraic effect is essentially an interface comprising a set of related operations. Programs written against such interfaces are represented as abstract syntax trees whose nodes represent effectful operations. These syntax trees are given by the following data type, commonly known as the free monad where Pure represents a value, and Op represents an operation given by a signature functor f:

data Free f a
  = Pure a
  | Op (f (Free f a))

The problem with higher-order operations is that it is not obvious how to represent the local operation as a signature functor that is compatible with Free. Consider:

data Reader r k
  = Ask (r -> k)
  | forall a. Local (r -> r) (X a) (a -> k)

The key question is: what is X here?

To match the MonadReader type class interface, it should be a syntax tree with the same effects as k. The problem is that Free does not support signature functors that match this type constraint!

It does, however, allow us to model local as a smart constructor:

local :: Ask r < f => (r -> r) -> Free f a -> Free f a

Here, the Ask effect, its smart constructors, and its handler is as follows:

data Ask r k
  = Ask (r -> k)
  deriving Functor

ask :: Ask r <: f => Free f r
ask = Op (inj (Ask Pure))

hAsk :: Functor f' => r -> Handler (Ask r) a f' a
hAsk r = Handler
  { ret = pure
  , hdlr = \x -> case x of Ask k -> k r }

The idea is that we can use Ask to implement local as an inline application of an effect handler, as follows:

local g m = do
  r <- ask
  handle (hRead (g r)) m -- ill-typed!

However, this definition of local is ill-typed. There are two problems.

First, recall that the type of handle from the previous blog post is:

handle :: (Functor f, Functor f')
       => Handler f a g b -> Free (f + f') a -> Free f' b

Using this, handle hAsk assumes that the Ask effect occurs as the first effect in a row. However, all that we know from the Ask r < f constraint is that the Ask effect occurs somewhere in f.

Second, the computation type resulting from calling handle (hAsk (g r)) m has fewer Ask effects than m does. But the type of local requires the computation type to have the same effects.

The rest of this blog post introduces infrastructure that addresses these two problems: functor isomorphisms witnessing that two functors are equivalent; functor forephisms witnessing that a functor is equivalently expressible as a functor sum; and finally an inline handling abstraction based on functor forephisms.

Encoding Higher-Order Effects

In order to encode higher-order effects we first recall some basic definitions from the previous blog post. If you read that already, or are familiar with it, you can skip the “Basics” section below.

Basics from Previous Blog Post

The Free data type is associated with the following notion of fold:

fold :: Functor f => (a -> b) -> (f b -> b) -> Free f a -> b
fold gen _   (Pure x) = gen x
fold gen alg (Op f)   = alg (fmap (fold gen alg) f)

Using this fold, we can transform signature functors (typically used to permute signature functor sums):

infixr 6 +
data (f + g) a
  = L (f a)
  | R (g a)
  deriving Functor

type f ->: g = forall a. f a -> g a

permute :: (Functor f, Functor f')
        => (f ->: f') -> Free f a -> Free f' a
permute f = fold Pure (Op . f)

The fold also lets us apply effect handlers:

data Handler f a f' b
  = Handler { ret  :: a -> Free f' b
            , hdlr :: f (Free f' b) -> Free f' b }

handle :: (Functor f, Functor f')
       => Handler f a f' b -> Free (f + f') a -> Free f' b
handle h = fold
  (ret h)
  (\x -> case x of
     L y -> hdlr h y
     R y -> Op y)

Functor Isomorphisms

Our goal is to define a notion of subtyping constraint f < g which lets us witness that g is isomorphic to a functor sum f + f' for some f'.

To this end, we will use the following record type to define isomorphisms between two functors f and g:

data f :<->: g = Iso { to :: f ->: g, from :: g ->: f }
{- which satisifies
     to . from = id
     from . to = id -}

The following convenience functions witness that isomorphisms are an equivalence relation (reflexive, symmetric, transitive), a congruence relation for functor sums, and that sums are commutative and associative.

The convenience functions use the following eliminator for functor sums:

sum :: (f a -> b) -> (g a -> b) -> (f + g) a -> b
sum f _ (L x) = f x
sum _ g (R x) = g x

Now:

isoRefl :: f :<->: f
isoRefl = Iso id id

isoSym :: f :<->: g -> g :<->: f
isoSym i = Iso (from i) (to i)

isoTrans :: f :<->: g -> g :<->: h -> f :<->: h
isoTrans i1 i2 = Iso (to i2 . to i1) (from i1 . from i2)

isoSumCong :: f :<->: f' -> g :<->: g' -> (f + g) :<->: (f' + g')
isoSumCong i1 i2 = Iso
  (sum (L . to i1) (R . to i2))
  (sum (L . from i1) (R . from i2))

isoSumComm :: (f + g) :<->: (g + f)
isoSumComm = Iso
  (sum R L)
  (sum R L)

isoSumAssoc :: (f + (g + h)) :<->: ((f + g) + h)
isoSumAssoc = Iso
  (sum (L . L) (sum (L . R) R))
  (sum (sum L (R . L)) (R . R))

Forephisms and Functor Subtyping

A forephism between f and g witnesses that g is isomorphic to a functor sum with at least f:

data Forephism f g
  = forall f'. (Functor g, Functor f, Functor f') =>
      Forephism { iso :: g :<->: (f + f') }

Since a forephism between f and g is a witness that f is contained in g, we can use forephisms to represent subtyping relationships:

infixr 4 <:
class (Functor f, Functor g) => f <: g where
  forephism :: Forephism f g

This type class lets us “inject” functor sub types into super types:

inj :: f <: g => f a -> g a
inj = case forephism of
  Forephism i -> from i . L

We give similar functor subtyping instances as for the functor subtyping type class by the same name from the previous blog post on algebraic effects:

instance Functor f => f <: f where
  forephism = Forephism (Iso
    L
    (sum id (\(x :: End a) -> case x of)))

instance (Functor f, Functor g) => f <: f + g where
  forephism = Forephism isoRefl

instance (Functor f, Functor g, Functor g', f <: g')
      => f <: g + g' where
  forephism = case forephism of
    Forephism i -> Forephism
      (isoTrans
         (isoSumCong isoRefl i)
         (isoTrans isoSumComm (isoSym isoSumAssoc)))

These functor subtyping instances make use of the isomorphism convenience functions from earlier.

Inline Handling

We can use the functor subtyping type class to define a convenience function for inline effect handling. This convenience function makes use of effect masking:

mask :: Functor f => Free f a -> Free (f' + f) a
mask = fold Pure (Op . R)

Here mask says that the type of any computation can be weakened by introducing an effect interface that the computation does not in fact make use of.

The hup function below lets us apply a handler inline (that is, inside of a syntax tree) and mask that the resulting computation has fewer effects:

hup :: f <: g => (forall f'. Functor f' => Free (f + f') a -> Free f' b)
    -> Free g a -> Free g b
hup h = case forephism of
  Forephism i -> permute (from i) . mask . h . permute (to i)

Encoding local as an Inline Handler

We can now define a local function whose type signature coincides with the higher-order operation by the same name from the MonadReader interface:

local :: (Functor f, Ask r <: f) => (r -> r) -> Free f a -> Free f a
local f m = do
  r <- ask
  hup (handle (hAsk (f r))) m

The functional behavior of the function also coincides with the implementation of MonadReader provided by the instances in mtl.

However, we cannot easily change the implementation of the local operation in programs that use it, without either modifying them or changing the implementation of the local function in all programs that use it. In contrast, the implementation of operations in programs that use only algebraic effects without any inline applications of effect handlers can be changed by applying a different effect handler, without modifying programs.

Next: Defining Higher-Order Effects, Modularly

In the next blog post we generalize Free to support signature functors given by higher-order functors.

This generalization lets us define programs with higher-order effects as syntax trees.

Using algebras over these higher-order functors, we can modularly elaborate programs with higher-order effects into algebraic effects and inline handlers similarly to local, using the techniques described in this blog post.