Casper Bach Poulsen

Algebras of 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. As shown in part two of this blog post, we can apply effect handlers inside of abstract syntax trees to emulate higher-order effect interfaces. But that solution does not support modularly changing interface implementations without changing the programs that use them.

In this third and final part blog post on modeling effects in Haskell, 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, but for higher-order effects. The general solution we present in here builds on the techniques introduced in the previous two blog posts (1, 2).

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 or scoped effects. But (to the best of my knowledge) none that support higher-order effects in general.

The techniques in this blog post and the next are based on the POPL’23 paper on Hefty Algebras by Cas van der Rest and I. The paper uses Agda, which (similarly to other dependently typed programming languages such as Idris or Coq) relies on a static over approximation of strict positivity. Therefore our paper uses containers. Haskell does not enforce strict positivity via static checks, so we can represent higher-order effects in a way that exposes the underlying concepts in a more direct way. This blog post shows how.

Contents

The Problem with Higher-Order Effects

As summarized in the previous two blog posts (1, 2), higher-order effects are awkward to model using algebraic effects and handlers alone. For example, the higher-order operations local from 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 part one of the 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!

The previous blog post showed how to work around this problem by encoding a higher-order operation as a function in a style that is less modular than plain algebraic operations.

Here we present a more general solution. To this end we will use a more general notion of functor to represent signatures.

Higher-Order Functors and Hefty Trees

Recall that a functor in Haskell is a parameterized type f :: * -> * associated with a function fmap :: (a -> b) -> f a -> f b which satisfies the functor laws; i.e.:

class Functor (f :: * -> *) where
  fmap :: (a -> b) -> f a -> f b
  {- which satisfies
       fmap id       =  id
       fmap (f . g)  =  fmap f . fmap g -}

Instead of plain functors, we will use higher-order functors; i.e.:

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

class (forall f. Functor (h f)) => HOFunctor h where
  hmap :: (f ->: g) -> (h f ->: h g)
  {- which is a natural transformation; i.e.,
       hmap g . fmap f = fmap f . hmap g -}

We will use higher-order functors (or hofunctors for short) to define signatures of higher-order operations in syntax trees. In the following type—which we dub Hefty because it is Higher-order EFfecTY—the Return constructor represents a value, and Do represents a higher-order operation given by a signature functor h:

data Hefty h a
  = Return a
  | Do (h (Hefty h) (Hefty h a))

For a signature functor h :: (* -> *) -> (* -> *), the type h m k encodes the syntax of a higher-order operation whose parameter computations (i.e., the parameters of a computation type, such as the body in local f body) are of type m :: * -> *, and whose continuation (the remaining computation after the operation) is of type k :: *. So the application h (Hefty h) (Hefty h a) represents an operation whose parameter computations and continuation are both syntax trees comprising operations described by the signature hofunctor h.

Using this we can represent the Reader effect as a signature hofunctor:

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

deriving instance Functor (Reader r m)

instance HOFunctor (Reader r) where
  hmap _ (Ask k)       = Ask k
  hmap f (Local g m k) = Local g (f m) k

Here the standalone deriving instance uses Haskell’s StandaloneDeriving extension to derive the functor instance you would expect for Reader r m.

We can also generically lift any algebraic operation to a higher-order operation:

data A f (m :: * -> *) k = A (f k) deriving Functor

instance Functor f => HOFunctor (A f) where
  hmap _ (A x) = A x

And we can provide hofunctor sums similar to plain functor sums:

infixr 6 :+
data (h1 :+ h2) (m :: * -> *) k = HL (h1 m k) | HR (h2 m k)
  deriving Functor

instance (HOFunctor h1, HOFunctor h2) => HOFunctor (h1 :+ h2) where
  hmap f (HL x) = HL (hmap f x)
  hmap f (HR x) = HR (hmap f x)

Using these, we can represent programs involving both higher-order effects, such as Reader, and algebraic operations, such as the following Output effect whose signature functor, smart constructor, and handler is given below:

data Output x k = Out x k deriving Functor

out :: Output x <: f => x -> Free f ()
out x = Op (inj (Out x (Pure ())))

hOut :: Functor f' => Handler (Output x) a f' (a, [x])
hOut = Handler
  { ret = \x -> pure (x, [])
  , hdlr = \x -> case x of
      Out y k -> fmap (\(v,ys) -> (v,y:ys)) k }

In order to write these programs, we will use a hofunctor subtyping type class akin to the functor subtyping type class from the previous blog post.

First, we lift the notion of functor isomorphism to higher-order functor isomorphism, and the notion of functor forephism to higher-order functor forephisms:

type h1 :-> h2 = forall (m :: * -> *) k. h1 m k -> h2 m k

data h1 <-:-> h2 = HOIso { hoto :: h1 :-> h2, hofrom :: h2 :-> h1 }
{- which satisifies
     hoto . hofrom = id
     hofrom . hoto = id -}

data HOForephism h1 h2
  = forall h3. (HOFunctor h1, HOFunctor h2, HOFunctor h3) =>
      HOForephism { hoiso :: h2 <-:-> (h1 :+ h3) }

Using these, the notion of subtyping is entirely analogous to the previous blog post:

infixr 4 :<
class (HOFunctor h1, HOFunctor h2) => h1 :< h2 where
  hoforephism :: HOForephism h1 h2

hoinj :: h1 :< h2 => h1 m a -> h2 m a
hoinj = case hoforephism of
  HOForephism i -> hofrom i . HL

We also implement the following instances entirely analogously to the previous blog post:

instance HOFunctor h => h :< h
instance (HOFunctor h1, HOFunctor h2) => h1 :< h1 :+ h2
instance (HOFunctor h1, HOFunctor h2, HOFunctor h3, h1 :< h3)
      => h1 :< h2 :+ h3

We use functor subtyping to define smart constructors for Reader:

ask :: Reader r :< h => Hefty h r
ask = Do (hoinj (Ask Return))

local :: Reader r :< h => (r -> r) -> Hefty h a -> Hefty h a
local f m = Do (hoinj (Local f m Return))

We can also generically lift smart constructors of algebraic effects to higher-order effect trees by folding over Free.

a :: (A f :< h, Functor f) => Free f a -> Hefty h a
a = fold Return (Do . hoinj . A)

However, if we use a to write programs as in the localout0 program below, Haskell’s type inference will not be able to infer what f is.

localout0 :: Hefty (Reader Int :+ A (Output Int) :+ A End) ()
localout0 = local (+ (1 :: Int)) (do
  (i :: Int) <- ask
  a (out i)) -- Haskell does not infer that `f` is `Output Int` here

We can aid Haskell’s type inference and provide more type hints if we specialize the type of a for particular effects; for example, for the Output effect:

oa :: A (Output Int) :< h => Free (Output Int) a -> Hefty h a
oa = a

Using the Monad instance of Hefty which we omit for now but show and explain later in this blog post:

localout :: Hefty (Reader Int :+ A (Output Int) :+ A End) ()
localout = local (+ (1 :: Int)) (do
  (i :: Int) <- ask
  oa (out i))

This localout program demonstrates how generalizing from Free to Hefty lets us define computations involving higher-order operations and effects as abstract syntax trees, akin to how we defined computations involving algebraic operations and effects in the first blog post.

Next, we show how this representation lets us give meaning to higher-order operations by providing composable elaborations that desugar higher-order operations into inline applications of effect handlers akin to the inline applications we used in the previous blog post. Unlike the previous blog post, the elaborations we will present here are factored into an interface given by a signature hofunctor.

This factoring makes it possible to change the implementation of higher-order operations for a particular program, without modifying the program itself, and without affecting the meaning of those operations anywhere else.

Algebras of Higher-Order Operations

The meaning of higher-order effects is given by a hofunctor algebras, given by the following data type:

data h :=> g
  = HA { ha :: forall a. h g (g a) -> g a }

We use such algebras to fold over hefty trees:

hfold :: HOFunctor h
      => (forall a. a -> g a)
      -> h :=> g
      -> (Hefty h ->: g)
hfold gen _   (Return x) = gen x
hfold gen alg (Do x)     =
  ha alg (fmap (hfold gen alg) (hmap (hfold gen alg) x))

This hfold function folds Hefty into a functor g. Later, we will also provide a generalized fold which lets us fold Hefty into any value. For now, this notion of algebra and fold suffices to define the meaning of higher-order effects by elaborating them into algebraic effects.

For example, the following algebra generically elaborates any algebraic effect given by a signature functor g into a computation Free f where g is a subtype of f:

eA :: g <: f => A g :=> Free f
eA = HA (\(A x) -> Op (inj x))

We can also provide an elaboration of the higher-order Reader effect into an algebraic effect AAsk effect. We first define the algebraic AAsk effect in terms of the following signature functor, smart constructor, and handler:

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

aask :: AAsk r <: f => Free f r
aask = Op (inj (AAsk Pure))

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

Using these, following algebra elaborates any Reader effect into a computation that has at least the AAsk effect, by applying an inline handler for aask to pass down a modified readable value:

eReader :: AAsk r <: f => Reader r :=> Free f
eReader = HA (\x -> case x of
  Ask k       -> aask >>= k
  Local f m k -> do
    r <- aask
    hup (handle (hAAsk (f r))) m >>= k)

We can run a computation by first elaborating all higher-order effects into plain algebraic effects and then run handlers. To do so, it is useful to compose algebras using algebra composition (/\):

infixr 6 /\
(/\) :: h1 :=> g -> h2 :=> g -> (h1 :+ h2) :=> g
a1 /\ a2 = HA (\x -> case x of
  HL x -> ha a1 x
  HR y -> ha a2 y)

For example, the following function lets us run the localout program from before:

run :: Hefty (Reader Int :+ A (Output Int) :+ A End) a -> (a, [Int])
run x = let
    y :: Free (AAsk Int + Output Int + End) _
      = hfold Pure (eReader /\ eA /\ eA) x   -- first elaborate
  in un (handle hOut (handle (hAAsk 41) y))  -- then handle

Now:

run localout == ((), 42)

It is also possible to assign a different meaning to the Reader effect to use a State effect to pass down a different local value. The signature functor, the smart constructors, and handler for State are:

data State s k = Put s k | Get (s -> k) deriving Functor

get :: State s <: f => Free f s
get = Op (inj (Get Pure))

put :: State s <: f => s -> Free f ()
put s = Op (inj (Put s (Pure ())))

hState :: Functor g => Handler_ (State s) a s g (a, s)
hState = Handler_
  { ret_ = \x s -> pure (x, s)
  , hdlr_ = \x s -> case x of
      Put s' k -> k s'
      Get k -> k s s }

Here is an alternative elaboration:

eReader' :: State Int <: f => Reader Int :=> Free f
eReader' = HA (\x -> case x of
  Ask k       -> get >>= k
  Local f m k -> do
    (i :: Int) <- get
    put (f i)
    v <- m
    put i
    k v)

To evaluate a local f m operation, we first get the old state and then mutate it (put (f i)) before evaluating m. Before evaluating the continuation, we put the old state.

The run' function below demonstrates how we can use this alternative eReader' elaboration to change the semantics of the local effect, without modifying localout, and without modifying the existing run function.

run' :: Hefty (Reader Int :+ A (Output Int) :+ A End) a -> ((a, Int), [Int])
run' x = let
    y :: Free (State Int + Output Int + End) _
      = hfold Pure (eReader' /\ eA /\ eA) x  -- first elaborate
  in un (handle hOut (handle_ hState y 41))  -- then handle

Now:

run' localout == (((), 41), [42])

This demonstrates how algebras of higher-order operations lets us modularly change interface implementations of higher-order effects; similarly to how we can modularly change interface implementations of algebraic effects.

A Monadic Bind for Hefty Trees

The localout program from earlier made use of monadic bind for sequencing Hefty computations. In part one of this blog post we showed how the monadic bind of Free is given by a fold over Free. It is tempting to try using hfold to the same end for Hefty.

However, hfold alone does not suffice. The monadic bind we are after has type

(>>=) :: Hefty h a -> (a -> Hefty h b) -> Hefty h b

But the type of hfold is:

hfold :: HOFunctor h
      => (forall a. a -> g a)
      -> h :=> g
      -> (Hefty h ->: g)

Here ->: is a type preserving function (or natural transformation); i.e.:

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

The only way we can use a ->: to turn a Hefty h a into a Hefty h b is to choose g to be a constant functor; e.g.:

newtype CHefty h a b = CHefty { unCHefty :: Hefty h a } deriving Functor

But that will only work for hefty trees whose sub-computations are guaranteed to have the same constant return type a. This assumption does not hold in general. To implement monadic bind for hefty trees, we need a more general recursion principle than hfold.

To this end, we can define a recursion principle inspired by Yang et al.’s functorial algebras. This recursion principle uses the same generator and algebra as hfold does, in addition to a base generator function of type (a -> b) and a base algebra of type (h g b -> b):

ffold :: HOFunctor h          -- as hfold
      => (forall c. c -> g c) -- as hfold
      -> h :=> g              -- as hfold
      -> (a -> b)             -- base generator
      -> (h g b -> b)         -- base algebra
      -> Hefty h a
      -> b
ffold _   _ genb _  (Return x) = genb x
ffold gen a genb ab (Do x) =
  ab                                    -- 3.
     (hmap (hfold gen a)                -- 2.
       (fmap (ffold gen a genb ab) x))  -- 1.

The Return case uses the base generator. In order to fold a Do node into a b value, ffold relies on a three step process:

  1. Recursively call ffold on the continuation to turn h (Hefty h) (Hefty h a) into h (Hefty h) b.
  2. Use the hfold to turn turn the sub-branches of signature hofunctor of type h (Hefty h) b into h g b.
  3. Apply the base algebra to turn h g b into b.

Using ffold we can implement the Monad, Applicative, and Functor instances of Hefty h.

instance HOFunctor h => Monad (Hefty h) where
  m >>= k = ffold Return (HA Do) k Do m

instance HOFunctor h => Applicative (Hefty h) where
  pure = Return
  f <*> m = ffold Return (HA Do) (flip fmap m) Do f

instance HOFunctor h => Functor (Hefty h) where
  fmap f = ffold Return (HA Do) (pure . f) Do

Conclusion

There are many more examples of higher-order effects than the simple Local effect discussed in this blog post. For example, exception catching, logic programming, effectful λs, and more.

The idea that we have presented in this blog post is that we can treat higher-order operations as an interface whose implementation is generally given by elaborating the interface into effects and handlers. Since effects and handlers can be used to implement continuations (in particular, call/cc), they can be used to represent any monadic effect, following Filinski.

There are other approaches to defining higher-order effects using effect handlers, such as scoped effects. Whereas hefty algebras involve a layer of indirection (elaborating into algebraic effects which we then handle), scoped effect handlers can give a semantics of the subset of higher-order effects known as scoped effects more directly. This suffices to give a modular and concise definition of many higher-order effects. But not all. In particular, effectful λs is not a scoped effect. Using hefty algebras we can define a broader class of effects in a manner that is equally modular as algebraic effects.