# Free monads of free monads

Yo dawg, I herd you like free monads…

It is well known that a free monad is a monad. It is less known that the free monad functor, that thing which generates free monads, is also a monad. Let us explore that idea in Haskell. After setting up a background of *indexed types*, *the monad of free indexed monads* will be introduced. Ways of smashing free monads into themselves will be attempted, in compliance with all rules of type-safety.

A category theorist says: obviously, every adjunction gives rise to a monad.

## Extensions and import used in this Literate Haskell post.

```
{-# LANGUAGE
-- This should really be standardized
InstanceSigs,
BlockArguments,
LambdaCase,
ScopedTypeVariables,
TypeOperators,
-- Deriving
DeriveFunctor,
DerivingVia,
StandaloneDeriving,
-- Types
DataKinds,
PolyKinds,
RankNTypes,
GADTs,
TypeFamilies,
FlexibleInstances
-- How strange it is that this pragma can contain comments.
#-}
module FreeFree where
import Control.Applicative (WrappedMonad(..), Const)
import Data.Kind (Type)
```

## Free monads

We will use the “freer monad”, a.k.a. “operational monad”, for simplicity.^{1}

```
data Free :: (Type -> Type) -> Type -> Type where
Pure :: a -> Free f a
Impure :: (x -> Free f a) -> f x -> Free f a
```

That type provides the raw ingredients of a *free monad*, but there’s a recipe to follow to make it edible, uh, I mean, to provide the minimal amount of functionality to convince people (or ourselves) that what we’ve got is actually a free monad.

The steps to show that `Free f`

is a free monad with respect to `f`

can be summarized as follows (with concrete type signatures just below).

`Free f`

is a monad.- There is a function
`call`

which defines the “primitive operations” in the monad. - There is a function
`interpret`

which extends a “interpretation” of those primitive operations, to an interpretation of whole`Free f`

programs (which use these operations).

```
{- The free monad starter pack -}
instance Monad (Free f) -- 1
call :: f ~> Free f -- 2
interpret :: Monad m => (f ~> m) -> (Free f ~> m) -- 3
```

The tilde-arrow `(~>)`

constructs types of *indexed functions*^{2}, functions between *indexed types*. The notation makes for some cute types, but I hope the natural power of indexed types will show through it.

The next section presents the definitions corresponding to the above three points. It is mostly a refresher, as there is a lot of existing introductory material on free monads elsewhere. Readers already comfortable with the concepts may skip this short section.

See also:

*Why free monads matter*, by Gabriel Gonzalez.*The operational monad tutorial*, by Heinrich Apfelmus.*Free and freer monads*, by Oleg Kiselyov.

### What makes a free monad

First, we have a monad: the type `Free f`

is equipped with `pure`

and `(>>=)`

(“bind”) functions satisfying the monad laws.

```
instance Monad (Free f) where
return :: a -> Free f a
return = Pure -- "return" is another name for "pure"
(>>=) :: Free f a -> (a -> Free f b) -> Free f b
Pure x >>= k = k x
Impure h u >>= k = Impure ((>>= k) . h) u
```

In Haskell, the `Monad`

type class is a subclass of `Functor`

and `Applicative`

, so we must also declare instances for those classes, which we shall ask to be derived. There are practical reasons for this organization, but it has little conceptual value for our story.

```
-- Deriving Functor and Applicative
deriving instance Functor (Free f)
deriving via WrappedMonad (Free f)
instance Applicative (Free f)
```

Second, there is a function from `f`

to `Free f`

. The type `f`

can be viewed as an interface of “operations”, or “effects”. We “call” or “perform” operations using this function.

With `call`

thus providing primitive operations, and with `pure`

and `(>>=)`

to compose them, a free monad is a fine language to write programs in.

Third and last: for any monad `m`

and any function `f ~> m`

, there is a monad morphism `Free f ~> m`

(i.e., a function which commutes with `pure`

and `(>>=)`

).

Concretely, it is a fold of the recursive type `Free f`

, a catamorphism of some sort.

Abstractly, the resulting function `Free f ~> m`

is an *interpretation* of programs in the `Free f`

monad into another monad `m`

, generated from an interpretation `f ~> m`

for the individual operations described by `f`

.

```
interpret :: Monad m => (f ~> m) -> (Free f ~> m)
interpret _ (Pure x) = pure x
interpret h (Impure k u) = h u >>= (interpret h . k)
```

Free monads have a *universal property* relating `call`

and `interpret`

: for any monad `m`

and any indexed function `h :: f ~> m`

, the monad morphism `interpret h`

is the unique solution of the following equation with unknown `i :: Free f ~> m`

:

In this post, we will skip the verification of these properties (“left as an exercise for the reader”).

### Monad of free monads

Since `Free g`

is a monad, we can specialize `interpret`

with `m = Free g`

:

The types of `call`

and `interpret`

are reminiscent of `pure`

and `(>>=)`

(actually, `flip (>>=)`

). Line them up and contemplate.

```
pure :: Monad m => a -> m a
call :: f ~> Free f
flip (>>=) :: Monad m => (a -> m b) -> ( m a -> m b)
interpret :: (f ~> Free g) -> (Free f ~> Free g)
```

Indeed, `Free :: (Type -> Type) -> (Type -> Type)`

, when viewed as a functor between indexed types, is a monad. It is a monad which maps an indexed type to its free monad: we can call it the *monad of free monads*.

## Indexed types

`Free`

is a monad, but not of the kind represented by the standard `Monad`

class. This class represents monads in the category of types and functions, and we are now looking at categories of indexed types and indexed functions.

In fact, we will now leave monads aside for a while to investigate those ubiquitous indexed types on their own.

An indexed type is a type with a parameter (or index), in other words, a function `k -> Type`

for some *index kind* `k`

.

The most common source of examples is with index kind `k = Type`

, that includes functors (`Maybe`

, `[]`

, `(,) a`

, `IO`

, `(->) a`

) but is totally not restricted to them; any `Type -> Type`

will do, e.g., `Endo`

, or `(:~:) a`

.

Regular, unindexed types can be seen as indexed types where `k = ()`

. Indeed, `() -> Type`

is isomorphic to `Type`

(with `Const`

being half of the isomorphism).

Indexed types can also have many indices, but that is equivalent to one index which is a tuple. In fact, we can define `curry`

and `uncurry`

as functions on types.

```
newtype Uncurry :: (a -> b -> Type) -> ((a, b) -> Type) where
UncurryOf :: f (Fst ab) (Snd ab) -> Uncurry f ab
data Curry :: ((a, b) -> Type) -> a -> b -> Type where
CurryOf :: f ab -> Curry f (Fst ab) (Snd ab)
```

These definitions use two type families `Fst`

and `Snd`

for the pair projections. In type-level programming^{3}, manipulating product types via projections somehow solves many problems that one frequently encounters otherwise with naive pattern-matching.^{4}

```
type family Fst (p :: (a, b)) :: a where
Fst '(x, _) = x
type family Snd (p :: (a, b)) :: b where
Snd '(_, y) = y
```

`Uncurry`

converts binary indexed types to unary.

```
(,) :: Type -> Type -> Type
Uncurry (,) :: (Type, Type) -> Type
Const :: Type -> k -> Type
Uncurry Const :: (Type, k) -> Type
```

### Indexed functors

We can also generalize the notion of functor. The standard `Functor`

class represents functors between types. This new `Functor1`

class represents functors between indexed types, or *indexed functors* for short.

```
-- Indexed functors
class Functor1 (w :: (k -> Type) -> (l -> Type)) where
map1 :: (p ~> q) -> (w p ~> w q)
-- Laws:
-- map1 id = id
-- map1 f . map1 g = map1 (f . g)
```

(It is a close sibling of the `Functor`

from the *rank2classes* library.)

It may help some readers to spell out the categories involved. For every index `k`

, there is a category where objects are indexed types `f, g`

of kind `k -> Type`

, and arrows are indexed functions `f ~> g`

. Note that the `Functor1`

class may represent functors between different source (`k -> Type`

) and target categories (`l -> Type`

) of indexed types. This contrasts with `Functor`

which only represents endofunctors on the one category of `Type`

.

Regarding type variable naming, the variables `w`

, `v`

will be of some kind `(k -> Type) -> (l -> Type)`

, and `f, g, p, q`

of kind `k -> Type`

. We use `p`

and `q`

here to avoid confusion when comparing indexed and unindexed type signatures (for example `Functor`

already uses `f`

as the instance head).

As said above, regular types are indexed types with `k = ()`

. For a bit of finger practice, find two types `ToFunctor1`

and `ToFunctor`

with two instances:

What are their kinds?

## Show the definitions of `ToFunctor`

and `ToFunctor1`

The kind of `ToFunctor1`

can keep a general `k`

kind variable, though this indexed functor must have the same domain and codomain.

Intuitively, `ToFunctor`

and `ToFunctor1`

are type-level functions, but we declare them as their own types instead of type synonyms to work with type classes.

```
-- w___________________________ a___
newtype ToFunctor :: ((() -> Type) -> (() -> Type)) -> (Type -> Type) where
WrapToFunctor :: w (Const a) '() -> ToFunctor w a
-- ToFunctor w a = w (\_ -> a) '()
-- f___________ p________ a
newtype ToFunctor1 :: (Type -> Type) -> ((k -> Type) -> (k -> Type)) where
WrapToFunctor1 :: f (p a) -> ToFunctor1 f p a
-- ToFunctor1 f p a = f (p a)
```

Interestingly, a functor between indexed types is itself an indexed type, with two indices. We can wrap it in `Uncurry`

to get a singly-indexed type:

Functors, functors between functors, and so on, all of them fit in the same world of (singly-)indexed types with enough Curry.

#### Indexed recursive types

While we’re not on the topic of monads, `Free`

is basically a variant of `Fix`

, a fixpoint operator for types.

```
-- Fixed point of f: (Fix f) is isomorphic to (f (Fix f))
newtype Fix (f :: Type -> Type) = Fix (f (Fix f))
```

Recursive types thus constitute one fundamental aspect of free monads. Two concrete examples of indexed functors appear here; things get pretty abstract afterwards.

Let’s first review what we can do with unindexed recursive types. For example, a type of arithmetic expressions…

… can be redefined as a fixed point of a functor `ArithF`

, called its “base functor”.

One way this encoding is useful is that functors such as `ArithF`

can be composed, forming new recursive types in a modular way; for example, we can thus add a constructor for multiplication to the language `ArithF`

:

```
data MulF a = Mul a a
-- Arithmetic expressions extended with multiplication
type ArithWithMul = Fix (ArithF :+: MulF)
```

This modularity of types extends to functions: we can define the meaning of operations in different functors independently, and compose them into the meaning of a whole language. See also the paper *Data Types à la Carte*, by Wouter Swierstra.

However, problems arise when the language becomes less “uniform”, which typically happens with the addition of types or binders.

#### Typed expressions with indexed functors

For example, assume we want to extend our arithmetic language with booleans by declaring constructs for boolean constants and conditionals:

```
data ConditionalF a
= Boolean Bool
| If a a a
-- Untyped Boolean and Arithmetic expressions
type UBArith = Fix (ArithF :+: ConditionalF)
```

Unfortunately, ill-typed terms plague that type such as `True + 3`

or `if 99 then False else 0`

.

A conventional solution to make those terms unrepresentable is a GADT indexed by the type of the expression:

```
-- (Typed) Boolean and Arithmetic expressions
data BArith :: Type -> Type where
Number :: Int -> BArith Int
Add :: BArith Int -> BArith Int -> BArith Int
Boolean :: Bool -> BArith Bool
If :: BArith Bool -> BArith a -> BArith a -> BArith a
```

But that type cannot be expressed as the fixed point of a `Functor`

, because the type `BArith`

has a non-uniform structure: its recursive occurences have different indices.

To fix this problem, whereas the encoding of recursive types via `Fix`

abstracted the recursive occurrences of a `Type`

, we can instead abstract recursive occurrences of the type constructor `BArith`

alone, of kind `Type -> Type`

, leaving the type indices untouched.

```
data BArithF :: (Type -> Type) -> Type -> Type where
Number :: Int -> BArithF f Int
Add :: f Int -> f Int -> BArithF f Int
Boolean :: Bool -> BArithF f Bool
If :: f Bool -> f a -> f a -> BArithF f a
```

The indexed type `BArith`

is indeed a fixed point of that indexed functor `BArithF`

, with the following indexed variant of `Fix`

to tie the knot. Unlike `Functor1`

, we are now restricted to endofunctors (“fixed point” doesn’t make sense otherwise).

```
-- Fixed point of w: (Fix1 w) is isomorphic to (w (Fix1 w))
data Fix1 (w :: (k -> Type) -> (k -> Type)) :: k -> Type where
WrapFix1 :: w (Fix1 w) a -> Fix1 w a
-- w (Fix1 w) ~> Fix1 w
-- would be equivalent,
-- but GHC doesn't like this syntax.
type BArith = Fix1 BArithF -- :: Type -> Type
```

Comparing the kind of `Fix1`

above with `Fix :: (Type -> Type) -> Type`

, we can see that we have replaced every `Type`

with `k -> Type`

.

Exercise: write the `Functor1`

instance for `BArithF`

.

`Functor1`

instance for `BArithF`

It looks just like a `Functor`

instance.

#### Statically checked binders: lambda calculus

Similarly, the exemplary language of anonymous functions, the lambda calculus, might look like this in the unindexed world:

```
data LambdaF a
= Var Var -- x (variable)
| App a a -- f e (application)
| Lam Var a -- \x -> e (abstraction)
type Lambda = Fix LambdaF
```

The issue with that representation is that it doesn’t guarantee variables are properly bound, and it offers no safety regarding variable capture.

Like in the previous section, a nice solution is to keep track the free variables of a term in its type, resulting in a typed De Bruijn representation. Interestingly, this does not require GADTs, only polymorphic recursion. Despite it’s name, that is a rather benign type-system feature, baked in Haskell since about forever.

Exercise: define an indexed functor `LambdaF`

such that `Fix1 LambdaF`

is isomorphic to `Lambda`

.

## Definition of the indexed `LambdaF`

## Indexed monads

We now present the indexed generalization of the `Monad`

class: monads in a category of indexed types, *indexed monads*.^{5} We flip `(>>=)`

to avoid an explicit quantification over an index `a :: k`

. At the same time, its nature as a natural transformation becomes more apparent, which also helps to see generalizations to “higher” categories. I like to name it `subst`

, as substitution is a common source of intuition for monads.

```
-- Indexed monads
class Monad1 (w :: (k -> Type) -> (k -> Type)) where
pure1 :: p ~> w p
subst1 :: (p ~> w q) -> (w p ~> w q)
-- Laws:
-- subst1 pure1 = id
-- subst1 k . pure1 = k
-- subst1 h . subst1 k = subst1 (subst1 h . k)
```

At the beginning, we witnessed that `Free`

is an indexed monad, which we can now record in the following instance.

```
instance Monad1 Free where -- k = Type
pure1 :: p ~> Free p
pure1 = call
subst1 :: (p ~> Free q) -> (Free p ~> Free q)
subst1 = interpret
```

By definition, the `Free f`

monad is a free monad (with respect to the indexed type `f`

). What about the indexed monad `Free`

we just defined? What does a free indexed monad even look like?^{6}

## Free indexed monads

### From `Fix`

to `Free`

As we’ve seen in the section on indexed recursive types, `Fix ArithF`

is the type of arithmetic expressions, with constructs given by the base functor `ArithF`

. Furthermore, `Free`

is almost like `Fix`

: `Free ArithF a`

is the type of arithmetic expressions with “holes” of type `a`

. If we set `a = Void`

, the empty type, `Free ArithF Void`

(“no holes”) is isomorphic to `Fix ArithF`

. The function `(>>=)`

fills those holes with expressions: that is substitution.

A straightforward definition of `Free`

is thus to extend `Fix`

with a constructor for those holes. The following `FFree f a`

is isomorphic to `Fix (f :+: Const a)`

; it is `Free`

in the *free* library:

```
-- Free monad (FFree f) with respect to the functor f
data FFree (f :: Type -> Type) (a :: Type)
= Pure a -- Hole
| Impure (f (FFree f a)) -- Fix-like constructor
```

Then the first `Free`

definition at the top of this post can be obtained by composing the `FFree`

we just defined with a free functor construction, also known as `Coyoneda`

^{7}: `Free f`

is isomorphic to `FFree (Coyoneda f)`

.

Once we have `Fix1`

, an indexed generalization of `Fix`

, we can extend it similarly with a new constructor, to get `FFree1`

generalizing `FFree`

.

```
-- Free indexed monad (FFree1 w) with respect to the indexed functor w
data FFree1
(w :: (k -> Type) -> (k -> Type))
(f :: k -> Type)
(a :: k)
= Pure1 (f a)
| Impure1 (w (Free1 w f) a)
```

Here also, we will switch to the “freer” variant to avoid headaches with the `Functor1`

constraints that `FFree1`

would incur. This transformation can also be understood in terms of an indexed generalization of `Coyoneda`

.

This is the *free indexed monad* we will be using in the rest of the post.

```
-- Free indexed monad (Free1 w) with respect to the indexed type w
data Free1
(w :: (k -> Type) -> (k -> Type))
(f :: k -> Type)
(a :: k) where
Pure1 :: f a -> Free1 w f a
Impure1 :: (g ~> Free1 w f) -> w g a -> Free1 w f a
```

### Free indexed monads

To demonstrate that `Free1 w`

is really a *free indexed monad*, we will follow the recipe given at the beginning for `Free f`

, adapted to indexed monads. As it turns out, the definitions are essentially the same as for `Free f`

, but with more squiggly arrows. Here, the extra polymorphism is handled completely invisibly by Haskell’s type system.

First, `Free1 w`

is an indexed monad.

```
instance Monad1 (Free1 w) where
pure1 :: p ~> Free1 w p
pure1 = Pure1
subst1 :: (p ~> Free1 w q) -> (Free1 w p ~> Free1 w q)
subst1 k (Pure1 x) = k x
subst1 k (Impure1 h u) = Impure1 (subst1 k . h) u
```

Second, there is a function `w ~~> Free1 w`

, which motivates the introduction of a double tilde-arrow for doubly-indexed functions.

```
-- Indexed functions with two indices (whereas (~>) is for one).
type v ~~> w = forall f a. v f a -> w f a
```

Third and last, given an indexed monad `v :: (k -> Type) -> (k -> Type)`

, for any function `w ~~> v`

, there is an indexed monad morphism `Free1 w ~~> v`

.

```
interpret1 :: Monad1 v => (w ~~> v) -> (Free1 w ~~> v)
interpret1 _ (Pure1 x) = pure1 x
interpret1 h (Impure1 k e) = subst1 (interpret1 h . k) (h e)
```

To recapitulate, we started with `Free`

:

`Free f`

is a (free) monad;`Free`

is an indexed monad, with`call`

and`interpret`

as its monadic operations.

Then we discovered `Free1`

:

`Free1 w`

is a (free) indexed monad.

There is an obviously missing piece:

`Free1`

is also an indexed monad, with two indices of kinds`k -> Type`

and`k`

, and with`call1`

and`interpret1`

as its monadic operations.

### Monad of free indexed monads

We cannot directly make `Free1`

an instance of `Monad1`

, because it has the wrong kind (their arities are different: `Free1`

is a ternary type while `Monad1`

expects a binary type). We must first wrap `Free1`

to have a compatible kind.

The wrapper is named `Unspice`

, because it “uncurries” the indexed type. Although the wrappers have scary kinds and bloat the code, they are purely a compile-time device to adjust the kinds of types. There is no runtime cost (in principle^{8}), and to understand how the code runs, we simply ignore the wrappers.

```
newtype Unspice ::
(((k -> Type) -> (k -> Type)) -> ((k -> Type) -> (k -> Type))) ->
((k -> Type, k) -> Type ) -> ((k -> Type, k) -> Type ) where
UnspiceOf :: Uncurry (ww (Curry w)) s -> Unspice ww w s
```

## Unwrapping functions

These wrappers become the identity function at run time, so we can ignore them in order to understand the behavior of functions.

The wrapped `Free1`

is thus named `Free1'`

. At a high level, we can think of it as identical to `Free1`

.

The kind of this wrapped `Free1`

is of the form `(h -> Type) -> (h -> Type)`

, as `Monad1`

expects; to be more specific, `h = (k -> Type, k)`

. Like the `Free`

indexed monad, `pure1`

and `subst1`

are actually defined as `call1`

and `interpret1`

, if we ignore the wrappers.

```
instance Monad1 Free1' where
pure1 :: p ~> Free1' p
pure1 = toUnspice . call1 . CurryOf
-- pure1 = call1 -- ignoring wrappers
subst1 :: forall p q.
(p ~> Free1' q) -> (Free1' p ~> Free1' q)
subst1 f = toUnspice . interpret1 f' . fromUnspice where
-- subst1 = interpret1 -- ignoring wrappers
f' :: Curry p ~~> Free1 (Curry q)
f' (CurryOf x) = fromUnspice (f x)
-- f' = f -- ignoring wrappers
```

In the definition of `subst1`

, we pull out `f'`

, a wrapped version of `f`

. Because it is a polymorphic function consuming a GADT (`Curry`

), it requires an explicit type signature, which refers to the type variables `p`

and `q`

bound at the top, thanks to `ScopedTypeVariables`

. The function `f'`

could also be inlined as an anonymous function, which wouldn’t need such a signature, though it seems messier in a different aspect.

That instance shows that `Free1`

is an indexed monad, while its image consists of free indexed monads: `Free1`

is the *indexed monad of free indexed monads*.

## Free monads of free monads

This all started with the observation that a free monad functor (`Free`

and `Free1`

) is a monad, thus dubbed *monad of free monads*. Let us tackle the final question on everyone’s mind: is that monad a free monad, so that we can talk of the *free monad of free monads*?

In other words, we are looking for some indexed type `Key`

(a *key* to free monads) such that `Free1 Key`

is isomorphic to `Free`

or `Free1`

.

Sadly, there doesn’t seem to be a solution, though I don’t have a solid proof right now. It might be possible in a fancier type system with equation-carrying types, and by that I mean higher-inductive types or quotient types, which are still subjects of active research.

Nevertheless, we can still try to construct an indexed type `Free1 Key`

with not all but most of the practical features of a monad of free monads.

### Free monads for semantics

The `Key`

we’re looking for is meant to be the interface of operations, or effects, of the free indexed monad `Free1 Key`

, but what operations?

Earlier, we established that `Free1`

and `Free1 w`

are both indexed monads. What about `Free1 w f`

, that is applied twice? In general, there is nothing we can say about it; it doesn’t even have the kind which `Monad`

expects (`Free1 w f :: k -> Type`

). Therefore, if `Free1 Key f`

is anything like the free monad `Free f`

, its monadic structure must come from `Key`

.

This suggests to define `(=<<)`

and `pure`

as *effects* of the free indexed monad `Free1 Key`

. We thus define `Key`

, using its first type parameter `f :: Type -> Type`

to refer to the type of computations handled by the *higher-order effect* `(=<<)`

.

```
data Key :: (Type -> Type) -> (Type -> Type) where
(:=<<:) :: (a -> f b) -> f a -> Key f b
-- (a -> m b) -> m a -> m b
PureK :: a -> Key f a
```

### Free monad of free pseudo-monads

The type `Free1 Key`

is actually isomorphic to the following recursive type, with constructors for `pure`

, `(>>=)`

, and `call`

. Although it tries hard to look like a monad, it satisfies none of the three monad laws^{9}: it is a *pseudo-monad*. We can thus recognize `Free1 Key f`

as a *free pseudo-monad*.

```
data Free1K f a where
(:=<<:.) :: (a -> Free1K f b) -> Free1K f a -> Free1K f b
Pure1K :: a -> Free1K f a
Call1K :: f a -> Free1K f a
```

However at the upper level, `Free1 Key`

(without the `f`

) is still a perfectly healthy free indexed monad: it is the *free indexed monad of free pseudo-monads*. To summarize:

`Free1 Key`

is a free indexed monad (with respect to`Key`

);`Free1 Key f`

is a free pseudo-monad (with respect to`f`

).

We can again follow the recipe of free monads for `Free1 Key f`

, ensuring that it is indeed a free pseudo-monad. Although the laws are not satisfied, the implementation still has some interesting details to show.

First, `Free1 Key f`

is a pseudo-monad.

Since the `Monad`

operations are actually provided as *effects* by `Key`

, both `return`

and `(>>=)`

are defined using `Free1`

’s `Impure1`

constructor.

```
instance Monad (Free1 Key f) where
return x = Impure1 id (PureK x)
u >>= k = Impure1 id (k :=<<: u)
-- Deriving Functor and Applicative
deriving via WrappedMonad (Free1 Key f)
instance Functor (Free1 Key f)
deriving via WrappedMonad (Free1 Key f)
instance Applicative (Free1 Key f)
```

Second, there is a function `f ~> Free1 Key f`

, to perform `f`

effects in the pseudo-monad `Free1 Key f`

.

The funny thing is that, while `return`

and `(>>=)`

were defined above as effects (`Impure1`

), `call`

is now defined as a pure action (`Pure1`

). Actually, this story started by identifying `call`

as `pure1`

, so this makes sense, totally.

Third, for every function `f ~> m`

, there is a pseudo-monad morphism `Free1 Key f ~> m`

.

The simplest implementation is an explicitly recursive fold of the `Free1 Key f`

tree. Replace `(:=<<:)`

with `=<<`

, `PureK`

with `pure`

, and type-tetris the rest until it typechecks.

```
interpret1K :: Monad m => (f ~> m) -> (Free1 Key f ~> m)
interpret1K h (Pure1 e) = h e
interpret1K h (Impure1 k (l :=<<: u))
= (interpret1K h . k . l) =<< interpret1K h (k u)
interpret1K _ (Impure1 _ (PureK x)) = pure x
```

But we already have a way to fold `Free1`

, that’s `interpret1`

. It would be a shame not to use it. Who cares whether that’s a sane thing to do?

#### Recursion schemes for recursion schemes

We need an indexed monad as a target for the fold `interpret1`

. It is possible to meticulously handcraft such an indexed monad, but here’s a hint out of left field: we have already seen a couple of indexed monads.

In fact, `Free`

is a pretty good candidate.^{10} To see why, specialize `interpret1`

with what we now have:

```
interpret1 :: Monad1 v => (w ~~> v ) -> (Free1 w ~~> v )
interpret1 :: (Key ~~> Free) -> (Free1 Key ~~> Free)
```

If we supply a suitable `Key ~~> Free`

function, we get to fold any `Free1 Key f`

into `Free f`

, which we already know how to interpret into another monad `m`

, given `f ~> m`

.

So we need to find `Key ~~> Free`

. The type `Key`

defines monadic composition as an “uninterpreted effect”, and `Free`

is a monad, so we can hope this makes sense. We pattern-match on the `Key`

and type-tetris our way out of each case. The function is named `legitimize`

because it interprets the pseudo-monad `Free1 Key`

into the monad `Free`

.

```
-- Equivalent signatures:
-- Free1 Key f a -> Free f a
-- Free1 Key f ~> Free f
legitimize :: Free1 Key ~~> Free
legitimize = interpret1 \case
k :=<<: u -> Impure (call . k) u
PureK x -> Pure x
```

The `PureK`

case looks reasonable, but `(:=<<:)`

is intriguing.

In this context we have `k :: a -> g b`

and `u :: g a`

, for some abstract type `g`

(and `a`

, `b`

), and we need to construct `Free g b`

. This `g`

comes from the universal quantification in `Key ~~> Free`

in the argument of `interpret1`

, that’s why `g`

is abstract. The only sensible action for us is to compose two `call`

(the first one is inlined and becomes `Impure`

) to `u`

and `k`

respectively. It is an oddly simple `Free g`

program to write.

Since `interpret1`

only knows about the `Monad1`

instance of `Free`

, we can expect it to call `subst1`

, i.e., `interpret`

, on that small program of two `call`

, to interpret `g`

into an actual monad. Intuition about parametricity and abstract nonsense tell me it’s probably doing the right thing, but it would be very interesting to work through the proof of correctness.

We finally obtain our alternative implementation of the `Free1 Key f`

interpreter, refactoring the main recursive fold into `interpret1`

and `interpret`

.

`legitimize`

thus takes us from `Free1 Key`

to `Free`

, and then `interpret`

from `Free f`

(a different monad from `Free`

!) to `m`

.

### Free monad of free indexed pseudo-monads

Now let’s repeat the process for `Free1`

. We will approximate `Free1`

as `Free1 Key1`

for some type `Key1`

, so that:

`Free1 Key1`

is a free indexed monad (with respect to`Key1`

);`Free1 Key1 w`

is a free indexed pseudo-monad (with respect to`w`

).

The code will be mostly the same as that of `Free1 Key`

we just saw, but with many wrappers to curry and uncurry indexed types. Here, typed holes were invaluable to remain sane.

The functor `Key1`

is the indexed analog of `Key`

: every `Type`

becomes `k -> Type`

, and we insert type indices where necessary.

```
data Key1 ::
((k -> Type) -> (k -> Type)) ->
((k -> Type) -> (k -> Type)) where
(:=<<:!) :: (p ~> w q) -> w p b -> Key1 w q b
-- (p ~> w q) -> (w p ~> Key1 w q )
PureK1 :: p a -> Key1 w p a
-- p ~> Key1 w p
```

We must then solve a kind mismatch, for similar reasons to those motivating `Unspice`

. The first parameter of `Free1`

must have a kind of shape `(h -> Type) -> (h -> Type)`

, which is binary (`h -> Type`

and `h`

), while `Key1`

is a ternary indexed type. We have to `Unspice`

(“uncurry”) the indexed type `Key1`

, so that we can apply `Free1`

to it, with `h = (k -> Type, k)`

.

Then, we must curry that back, with the `Spice`

wrapper below, so that `Spice (Free1 (Unspice Key1))`

has the same kind as `Key1`

, which is the kind one would expect of a monad of free indexed monads.

```
newtype Spice ::
(((k -> Type, k) -> Type ) -> ((k -> Type, k) -> Type) ) ->
((k -> Type) -> (k -> Type)) -> ((k -> Type) -> (k -> Type)) where
SpiceOf :: Curry (ww (Uncurry w)) f a -> Spice ww w f a
```

## Wrappers for `Spice`

.

We hide those wrappers with some synonyms. `Unspice`

and `Spice`

only do (un)currying, which doesn’t fundamentally alter the structure of `Key`

and `Free1 Key1'`

. At a high level, think of `Key1'`

and `Free1Key1'`

as identical to `Key1`

and “`Free1 Key1`

” (which is technically ill-typed without `Key1'`

).

Mirroring the situation for `Free1 Key`

, the type `Free1Key1'`

is the *free indexed monad of free indexed pseudo-monads*. It is isomorphic to this standalone recursive type, analog of `Free1K`

:

```
data Free1K1 ::
((k -> Type) -> (k -> Type)) ->
((k -> Type) -> (k -> Type)) where
Call1K1 :: w f a -> Free1K1 w f a
(:=<<:!.) :: (g ~> Free1K1 w f) -> Free1K1 w g a -> Free1K1 w f a
Pure1K1 :: f a -> Free1K1 w f a
```

Let’s run the free monad recipe again, for the fourth and last time, to verify that `Free1Key' w`

is a free indexed pseudo-monad.

First, `Free1Key1' w`

is an indexed pseudo-monad.

```
instance Monad1 (Free1Key1' w) where
pure1 :: p ~> Free1Key1' w p
pure1 x = toSpice (Impure1 id (toUnspice (PureK1 x)))
-- pure1 x = Impure1 id (PureK1 x) -- ignoring wrappers
subst1 :: forall p q.
( p ~> Free1Key1' w q) ->
(Free1Key1' w p ~> Free1Key1' w q)
subst1 k (SpiceOf (CurryOf u))
= toSpice (Impure1 id (toUnspice
((fromSpice . k) :=<<:! CurryOf u)))
-- subst1 k u = Impure1 id (k :=<<:! u) -- ignoring wrappers
```

Second, there is a function `w ~~> Free1Key1' w`

.

```
call1K1 :: w ~~> Free1Key1' w
call1K1 = toSpice . Pure1 . UncurryOf
-- call1K1 = Pure1 -- ignoring wrappers
```

Third, there is an interpreter into any indexed monad `v`

. We apply the idea from the previous section, to first interpret `Free1 Key1'`

into `Free1'`

(the indexed analog of `Free`

), and then use `Free1'`

’s interpreter to reach `v`

.

```
-- From the free indexed pseudo-monad Free1 Key1'
-- to the free indexed monad Free1'
legitimize1 :: Free1 Key1' ~~> Free1'
legitimize1
= interpret1 (toUnspice . h . fromUnspice)
where
h (k :=<<:! u) = Impure1 (call1 . k) u
h (PureK1 x) = Pure1 x
```

Hopefully by now you’re used to the feeling of déjà vu. Everything is the same as in the previous case, sprinkled with squiggly arrows and wrappers.

All recursion is hidden behind folds (`interpret1`

).

In `interpret1K1`

, the `legitimize1`

function first takes us from `Free1 Key1'`

to `Free1'`

, and then `interpret1`

takes us from `Free1 w`

(a different indexed monad from `Free1`

!) to `v`

.

```
-- Interpreter of the free indexed monad Free1Key1'
interpret1K1 :: forall w v.
Monad1 v => (w ~~> v) -> (Free1Key1' w ~~> v)
interpret1K1 h (SpiceOf (CurryOf u))
= (interpret1 h' . fromUnspice . legitimize1) u
-- interpret1K1 h
-- = interpret1 h . legitimize -- ignoring wrappers
where
h' :: Curry (Uncurry w) ~~> v
h' (CurryOf (UncurryOf x)) = h x
-- h' = h -- ignoring wrappers
```

There is something funny going on in the specialization of `interpret1`

used by `legitimize1`

: we are interpreting the free indexed monad `Free1 Key1'`

into `Free1`

, that is the very indexed monad which generates that free indexed monad we started from!

```
interpret1 :: Monad1 v => (w ~~> v ) -> (Free1 w ~~> v )
interpret1 :: (Key1' ~~> Free1') -> (Free1 Key1' ~~> Free1')
```

## The unreasonable effectiveness of types

The code after the introduction of `Unspice`

was largely driven by typed holes.

On the one hand, it is so abstract that it’s hard to follow what is going on in detail. On the other hand, there is much structure to rely on: the types are so precise that there is only one way forward most of the time, and recurrent patterns across the different sections further guide the implementation.

## Conclusion

This is the end of today’s story, though the journey continues.

I would certainly like to see how free indexed monads fare compared with other systems of higher-order effects (e.g., *Effect Handlers in Scope*, by Nicolas Wu et al.).

Those were four takes on “monads of free monads”, and two of them are themselves defined as free monads, although they actually generate pseudo-monads.

The indexed monad of free monads,

`Free`

.`Monad (Free f)`

`Monad1 Free`

The indexed monad of free indexed monads,

`Free1`

.`Monad1 (Free1 w)`

`Monad1 Free1'`

The free indexed monad of free pseudo-monads,

`Free1 Key`

.`Monad (Free1 Key f)`

`Monad1 (Free1 Key)`

(specialization of`Monad1 (Free1 w)`

)

The free indexed monad of free indexed pseudo-monads,

`Free1 Key1`

.`Monad1 (Free1Key1' w)`

`Monad1 (Free1 Key1)`

(specialization of`Monad1 (Free1 w)`

)

## Appendix A: I can handle myself

Another idea to wrap your head around.

At the level of unindexed monads, we can write the following function `iter`

, which repeats an action updating an `a`

state until it finishes with a `b`

.

The same combinator can be implemented for indexed monads.

```
iter1 :: Monad1 v => (f ~> v (f :+: g)) -> (f ~> v g)
iter1 run a = subst1 (either1 (iter1 run) pure1) (run a)
-- Indexed sum eliminator
either1 :: (f ~> h) -> (g ~> h) -> (f :+: g ~> h)
either1 l _ (L a) = l a
either1 _ r (R b) = r b
```

But remember that in the indexed world, the monadic bind of `Free`

is actually the interpretation of effects (`interpret`

). So the first argument of `iter1`

is really an effect handler `f ~> Free (f :+: g)`

, which is made to handle its own `f`

effects.

See also *Turing Completeness Totally Free* (PDF), by Conor McBride.

## Appendix B: Beware of bugs in the above code

I have not proved it correct, not even tried it.

Now that you mention it, it might be a good idea to test it at least once.

```
main :: IO ()
main = do
-- Test for Free1 Key
-- Should print [1,2,3,4,5]
print (interpret1K id do
tf <- call1K [True, False]
if tf then
call1K [1, 2, 3]
else
call1K [4, 5 :: Int])
-- There should also be a test for Free1Key1'...
```

Not the same as

`Free`

from the*free*library, which has a more complicated story because of the extra`Functor`

constraint on its functions. In this post, try to consider the difference between that and “freer” as a minor bureaucratic detail.↩Also called

*natural transformations*by some, but the mathematical meaning of the term commands too much structure, as it implies`f, g :: k -> Type`

are functors, and thus the domain`k`

is a category. As we will see, the index kind`k`

can be arbitrary (not only`Type`

), so it might not make sense as a category.↩Or simply “programming” as it is going to be called once everyone programs in Coq… That was a joke, of course. Everyone will prefer Agda.↩

To catch a glimpse of the problem, try to write a function of type

`f ~> Uncurry (Curry f)`

with a different version of`Uncurry`

or`Curry`

which uses the pair constructor`'(,)`

explicitly instead of`Fst`

and`Snd`

. This affair is also sort of related to the business of codata (blogpost by Javier Casas, linking to a paper by Paul Downen et al.).↩There are different variants of

*indexed monads*. This one first appears in*Kleisli Arrows of Outrageous Fortune*(PDF), by Conor McBride. With a pinch of singletons, those are nice monads for dependently-typed programming even pre-Dependent Haskell. A possibly more common kind of indexed monads is`i -> i -> Type -> Type`

, discussed in*Parameterized Notions of Computation*, by Robert Atkey, among many places. For example, it is used by the*motor*library for type-safe state machines. Graded monads, indexed by monoids, are also closely related.↩The notion of “free” is relative to a notion of “forgotten structure”, for

`Free`

, the base category would be that of indexed types with the kind of`Free`

:`((Type -> Type) -> (Type -> Type))`

.↩See also the blog post

*Yoneda intuition from humble beginnings*(reddit thread).↩Except for

`Curry`

because existential newtypes are not yet supported.↩There is actually a less naive

`Monad`

instance satisfying two of the laws, following the logic of a good free monad, in a type that’s too big to ever be one.↩Since I couldn’t give that hint to myself, I had to construct the right indexed monad from scratch. I found the free monad, but finally encoded, which doesn’t change much to this story.↩