```
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleContexts #-}
import Prelude hiding (Read, sum)
```

```
instance Functor f => Monad (Free f) where
Pure x >>= k = k x
Op f >>= k = Op (fmap (>>= k) f)
instance Functor f => Functor (Free f) where
fmap f (Pure x) = pure (f x)
fmap f (Op x) = Op (fmap (fmap f) x)
instance Functor f => Applicative (Free f) where
pure = Pure
Pure f <*> m = fmap f m
Op x <*> m = Op (fmap (<*> m) x)
```

`data End k deriving Functor`

# 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
= Op (inj (Ask Pure))
ask
hAsk :: Functor f' => r -> Handler (Ask r) a f' a
= Handler
hAsk r = pure
{ ret = \x -> case x of Ask k -> k r } , hdlr
```

The idea is that we can use `Ask`

to implement `local`

as an inline application of an effect handler, as follows:

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

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
Pure x) = gen x
fold gen _ (Op f) = alg (fmap (fold gen alg) f) fold gen alg (
```

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
= fold Pure (Op . f) permute 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
= fold
handle h
(ret h)-> case x of
(\x 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
= Iso id id
isoRefl
isoSym :: f :<->: g -> g :<->: f
= Iso (from i) (to i)
isoSym i
isoTrans :: f :<->: g -> g :<->: h -> f :<->: h
= Iso (to i2 . to i1) (from i1 . from i2)
isoTrans i1 i2
isoSumCong :: f :<->: f' -> g :<->: g' -> (f + g) :<->: (f' + g')
= Iso
isoSumCong i1 i2 sum (L . to i1) (R . to i2))
(sum (L . from i1) (R . from i2))
(
isoSumComm :: (f + g) :<->: (g + f)
= Iso
isoSumComm sum R L)
(sum R L)
(
isoSumAssoc :: (f + (g + h)) :<->: ((f + g) + h)
= Iso
isoSumAssoc 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
= case forephism of
inj 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 (Iso
forephism L
sum id (\(x :: End a) -> case x of)))
(
instance (Functor f, Functor g) => f <: f + g where
= Forephism isoRefl
forephism
instance (Functor f, Functor g, Functor g', f <: g')
=> f <: g + g' where
= case forephism of
forephism 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
= fold Pure (Op . R) mask
```

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
= case forephism of
hup h 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
= do
local f m <- ask
r 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.