Free Monad and Free Applicative using single Free type

Posted on 2018-02-20 by Oleg Grenrus

I define free Monad and free Applicative using single type, parametrised over a tensor. It's possible, because both Monad and Applicative are monoids in the category of endofunctors. There is little, if any, practical applications I can foresee for these definitions, but it's fun to see how things are connected. I won't prove laws hold, or constructions are free (= are left adjoint of a forgetful functor).

The post was inspired by Bartosz Milewski blog post about Free Monoidal Functors, and only while writing this I discovered Notions of Computations as Monoids, read that for rigid explanations.

Warning: plenty of infix operators ahead. Also formulas typeset with LaTeX.

#Introduction

Free applicative functors are free monoids where Day convolution is a tensor:

 \mathit{FreeA}\; F = \mu G. 1 + F \star G

On the other hand, free monads are also free monoids, but with function composition as monoidal product.

 \mathit{FreeM}\; F = \mu G. 1 + F \circ G

Note, lists are also free monoids where product is a Cartesian product (different category)!

 \mathit{List}\; A = \mu B. 1 + A \times B

So we can extract the common free monoid notion:

 \mathit{Free}_\otimes\; F = \mu G. 1 + F \otimes G

or

 \sum_{n\ge0} F^{\otimes n} = 1 + F + F \otimes F + F \otimes F \otimes F + \cdots

as in free monoid - ncatlab article.

Using \mathit{Free}_\otimes we can abstract over applicatives and monads (and lists):

 \begin{aligned} \mathit{FreeA} &= \mathit{Free}_\star \\ \mathit{FreeM} &= \mathit{Free}_\circ  \\ \mathit{List}  &= \mathit{Free}_\times \end{aligned}

Let's try to encode all of that in Haskell.

This blog post is a literate Haskell file. For this work we don't need a lot of extensions, they'd almost fit on one line.

#Free monoid in the category of endofunctors

Let's start by defining a free monoid. The definition resembles in shape the definition of lists, but is higher-order and parametrised over a tensor h and its unit i:

We could also used a FixH (as Bartosz does in his post) and separate FreeF algebra, but for our purposes splitting out recursion is not necessary, and would only clutter the presentation.

Next we need tensors. These definitions are unorthodox. Enlightened reader would guess why we use such variants. We will explain that in the respective sections.

Using Free we can right away define free Applicative and free Monad: Both tensors have Identity as a unit functor.

Let's see how to define the operations on Free. We can immediately define pure (or return), independently of choice of h or f:

As both free applicative and free monad are free monoids in category of endofunctors, it shouldn't be surprising that pure and return look like empty list. (Even there's a, there aren't any f).

Both Applicative and Monad instances can be defined in a very similar way using auxiliary classes HAppend and FromDay:

FromDay witnesses a tensor homomorphism from Day to h.

The long squiggly arrow is a transformation between Tensors:

Day can be converted to Day trivially:

HAppend is a generalization of ++ for our Free lists, happend appends two Free h "lists". We need such class as plumbing is different for different choices of h. (Here I really miss that we cannot use infix operator as a type variable!)

 \mathit{happend} : \mathit{Free}_\otimes\; F \otimes \mathit{Free}_\otimes\; F \to Free_\otimes F

The short squiggly arrows are natural transformations:

#Lifting and retracting

One interesting operation is lifting f a into a free structure. For that we need more structure from h, in particular left unitor intro1. Then we map 1 into Done, and wrap that into More. In other words that's a singleton for a list.

 \begin{aligned} \mathit{intro}_1 &: F \to F \otimes 1 \\ \mathit{Done} &: 1 \to \mathit{Free}_\otimes\; F \\ \mathit{More} &: F \otimes \mathit{Free}_\otimes\; F \to \mathit{Free}_\otimes\; F \end{aligned}

For this operation we show types of intermediate results:

 \begin{aligned} \mathit{fa} &: F \\ \mathit{intro}_1\; \mathit{fa} &: F \otimes 1 \\ \mathit{hbimap}\; \mathit{id}\; \mathit{Done}\; (\mathit{intro}_1\; \mathit{fa}) &: F \otimes \mathit{Free}_\otimes\; F \\ \mathit{More}\; (\mathit{hbimap}\; \mathit{id}\; \mathit{Done}\; (\mathit{intro}_1\; \mathit{fa})) &: \mathit{Free}_\otimes\; F \end{aligned}

Or in Haskell:

The last operation is retracting of a free structure, one can spot the resemblance with foldMap.

HApply "applies" or retracts the tensor. That doesn't work for all f, so we need a constraint. It carries natural transformations

 \begin{aligned} \mathit{hpure} &: 1 \to F  \\ \mathit{happly} &: F \otimes F \to F \end{aligned}

Or in Haskell terms:

#Examples

#Free Monad

The basic example for free monads is the restricted IO. First we define the operation type (note, not a Functor):

Test console writes output into Writer log, and always returns "yes" as an input.

The runnable example of reading an input once, writing it and "done", and returning the read value as result of the computation:

#Free Applicative

Free applicatives are used a lot in various parsers. For example a naive command line argument parser: First a type encapsulating an option (example as in Free Applicative Functors by Paolo Capriotti and Ambrus Kaposi)

Then we need a type for a value we need to parse, let's use simple User:

The example parser could look like:

And because the structure is static, we can not only run the parser, but also generate "help" message:

#Higher-order functors and tensors

In this section we define HBifunctor, Tensor and other related type classes.

As we deal with tensors which are (higher-order) bifunctors, we will need a variant of Bifunctor for higher order functors. In this post will have a special version, one where bfmap (a variant of fmap) requires only second argument to be Functor. The kind annotation for h isn't strictly required, but it's there to show that h is binary operations on types of kind * -> *. hbimap is a higher-order variant of bimap.

Using HBifunctor we can defined Functor instance for Free.

Some HBifunctors are Tensors. Tensor laws resembles monoidal ones: I h is a unit functor and h is associative up to isomorphism.

 \begin{aligned} F \otimes 1 &\cong F \\ 1 \otimes F &\cong F \\ (F \otimes G) \otimes H &\cong F \otimes (F \otimes H) \end{aligned}

See Wikipedia or ncatlab for more discussion.

Next we'll define two Tensors: function composition Comp and Day convolution Day.

#Day convolution

Day convolution (named after Brian Day) is a product in the category of endofunctors. We won't use kan-extensions definition but have slightly different one:

It and kan-extensions definition are isomorphic, we can convert back and forth:

Similarly to Comp (defined later), Functor (Day f g) requires Functor g, but not Functor f.

Day is HBifunctor:

Next we define rest of the instances for Day: it's a Tensor, HApply and Happend.

Day is a tensor, with Identity as a unit:

HApply and Happend instances are interesting, they show why we chose :<**>: name for the constructor. HApply needs Applicative constraint, and we use <**> in happly implementation:

HAppend instance is straight forward. Note how More case resembles the disassoc defined above.

One more point: kan-extensions Day has liftA2 as the "native" operation (you should think how Free Day "lists" would look like, if used this definition):

#Functor composition

In previous section we defined own version of functor composition.

That's a surprising choice, as Functor composition is usually defined as

We can convert between these definition quite freely:

The reason is that to make comparison with Day convolution more fair, we'll drop the requirement for Functor f. We can do this by wrapping f in (sliced in) Coyoneda.

So instead of

we have more relaxed context for Functor (Comp f g) instance:

And because of relaxed context, we can defined HBifunctor instance:

Instead of usual Free monad (which requires Functor f), with our Comp we will get a freer monad (which doesn't require Functor f). Free monad adds return and join operations (you still need fmap), where naive encoding of freer monad adds return and bind, thus doesn't requiring anything from the f.

The rest of this section is instance definitions.

Comp is a tensor with Identity as a unit:

The HApply requires a Monad as a constraint:

As in Day case, Happend instance for Comp shows why the constructor is named :>>=: (Also if we would use Compose from base, the operation would look like join).

The last thing to do is FromDay instance for Comp. Because Hask has rich structure, we can convert Day into Comp.

Compare that to

it's virtually the same.

#Bonus: Convert Applicative to Monad

As we represent free applicatives and free monads using same Free, it's quiet simple to map free Applicative to free Monad:

where hhoistFree changes the tensor:

#Bonus: Arrows

Let's look on tensors we have, They have similar structure:

The object \ \mathit{fga} : (F \otimes G) A can be split into fx : F X and xga : X \overset{\otimes G}{\Longrightarrow} A for some X.

This can be encoded in Haskell as another type-class:

where Combined is a specialized dependent sum:

We already spoiled a little: the reminder of "unconsing" f x, is an arrow! And they can be composed with >>>. Using this machinery we can define happend' differently, pushing the combination plumbing into implementation of >>>:

where elim2' is a specialised version of elim2 to help out the type-checker:

Now we only need to show that Comp and Day are instances of Uncons: The arrow for Comp is not so surprising, it's Kleisli:

The arrow for Day is less known, so called StaticArrow (it's an Arrow if g is an Applicative, Kleisli is an arrow if g is a Monad):

I think we can define Free also using a Path of Arrows and a first element. I leave that as an extended exercise for a reader. :)

#Bonus: Product

We defined Tensor so we can have other unit than Identity. We can use this now. The Product (pair) as a tensor with Proxy as a unit. The free monoid is a "list of f a".

Again, we don't use base Product, but a variant with embedded Coyoneda for first element. The mapping function is put into a new data type. This makes plumbing less tedious as Arrow Prod = ProdK:

Fixity definitions are important, as we don't need to write as many parentheses. We skip ahead to define HApply. What's the right constraint? Alternative feels like a good fit, but it has restrictive context (Applicative), so let's define a new class:

Note: Monoid1 class is deliberately agnostic to "left catch" vs. "left distribution". It's just a monoid. (See MonadPlus on wiki.haskell.org or documentation for Alt class).

The following example will use retractFree to extract the list of f a.

In theory, we could split Free into FixH and FreeF, and then make a fixed point of a composition of FreeF Day and FreeF Prod to build a free Alternative out of abstract non-senses. In practice you'd use something simpler or even completely custom thing (especially if you cannot have default many or some).

The rest of the section are instances, for completeness. Note that I Prod = Proxy. It's unusual use for Proxy!

#Conslusion & remarks

There is a lot of abstract nonsense in this post, hopefully you enjoyed and gained some new insights! Drop me a line on Twitter or Reddit.

Site proudly generated by Hakyll