Journal de Chaource's Journal

Free functors, free applicatives, free monads II
Part I
Consider the definitions (1), (2), and (3) of the "free monad" from the previous post,

Free₁ F t = Fix_s( t + F s )

Free₂ F t = Fix_S( t + F t + ∃a. S a * (a -> S t) )

Free₃ F t = Fix_s( t + ∃a. F a * (a -> s) )

Let us rewrite them in Haskell's "long form", that is, as representable functors, while giving the individual type constructors suggestive names:

data M₁ t where
Pure :: t -> M₁ t
Join :: F (M₁ t) -> M₁ t

data M₂ t where
Pure :: t -> M₂ t
Wrap :: F t -> M₂ t
Bind :: ∀a. ( M₂ a * (a -> M₂ t) ) -> M₂ t -- we replace ∃a by ∀a since we are moving it out of a contravariant position

data M₃ t where
Pure :: t -> M₃ t
Bind :: ∀a. ( F a * (a -> M₃ t) ) -> M₃ t

Then we notice two curious things:

- the type signatures of the "Pure" and "Bind" constructors are very similar to the types of the "pure" and "bind" methods of a monad:

pure :: ∀t. t -> M t
bind :: ∀t.∀a. M a -> (a -> M t) -> M t

The definition of the "free monad" looks almost like listing these two method's type signatures!

- however, the type "F a" is used in M₃ instead of "M a", and, as if to compensate this, there is an extra type constructor I called "Wrap", that injects "F a" into the free monad.

There is no doubt that all these definitions of the "free monad" are "correct" (i.e. both define a monadic functor). Questions remain: for instance, there are two places in the "bind" method where we use "M t" recursively. What if we wanted to use "F t" instead of "M t" in one of these places (or both)? There are four possibilities, of which two are not yet written down:

data M₄ t where
Pure :: t -> M₄ t
Bind :: ∀a. ( F a * (a -> F t) ) -> M₄ t

data M₅ t where
Pure :: t -> M₅ t
Bind :: ∀a. ( M₅ a * (a -> F t) ) -> M₅ t

Do these work, do they need additional type constructors to work, or do they fail even with additional constructors?

A partial answer was given in this blog post: http://blog.higher-order.com/blog/2013/11/01/free-and-yoneda/

The gist of that blog post is that M₃ is obtained from M₁ by using a "free functor" instead of a given functor F. So let us now look at how a "free functor" works.

(The "free functor" is sometimes called a "co-Yoneda", but so far I don't think the connection to the Yoneda lemma is at all helpful for understanding the "free functor".)

Free functors

A functor is a type constructor F with an additional morphism called "fmap" in Haskell.

fmap :: ∀t.∀a. F a -> (a -> t) -> F t

If we have a type constructor F that is not a functor, we can add some more structure around it and define a functor G like this:

G t = ∃a. F a * (a->t)

The type constructor G is a functor since it is exp-poly in "t" and uses "t" only in a contravariant position.

We call the functor G the "free F-functor".

It is then easy to see that M₁ applied to the free F-functor is the same as M₃ applied to the type constructor F.

The "Haskell long form" of the type definition is

data Ff₁ t where
Ffmap :: ∀a. F a * (a -> t) -> Ff₁ t

Note again the similarity of this and the type signature of "fmap". We just used the product F a * (a->t) -> Ff t instead of writing F a -> (a->t) -> Ff t, so that the implementation of this data type becomes more obvious.

Let us ask the same questions about the construction of the free F-functor as we asked about the construction of the free F-monad:

- How to derive this construction systematically?
- Can we replace "F s" by the recursive application of "Ff s" in the definition of "Ff" above? For instance, what about the alternative definition (inspired by comparing M₂ and M₃ above):

data Ff₂ t where
Wrap :: F t -> Ff₂ t
Ffmap :: ∀a. Ff₂ a * (a -> t) -> Ff₂ t

Is this definition equivalent to Ff₁?

To find answers, I found it helpful first to consider the concrete implementations of the two versions of the free F-functor according to definitions Ff and Ff₂.

Implementing the free functor

The "fmap" operation of the free F-functor is defined like this: We have a value (fa*g) of type Ff₁t, where fa : F a and g: a->t, and a function value h of type t -> s. We now define fmap on these two values in the only way possible:

fmap_Ff₁ (fa*g) h = fa * (h ∘ g).

So the value "fa" inside the product F a * (a->t) remains unchanged, but the morphism g gets composed with h.

Any value of type Ff₁t is therefore either created from scratch, where we supply some value "fa" of type "F a", or is obtained using "fmap", where this value "fa" remains unchanged.

It is natural to provide a "constructor" that injects a value of type F t into the free F-functor:

wrap :: F t -> Ff₁t
wrap ft = ft^{F t} * id^t->t

If values of type Ff₁t are always made either by this constructor or by fmap, then the initial value "ft" injected into Ff₁t will remain unchanged.

Note that we cannot "unwrap" a value of type Ff₁t because, even if we find that this value is of type F t * t->t, we cannot determine whether the function of type t->t is equal to identity.

Now, consider the second definition of the free F-functor. Now "Wrap" is part of the definition.

To define the function "fmap" as required for the functor instance, we now need to consider two cases. A value of Ff₂t can be either a "wrapped" F t or a "recursive case" Ff₂a * (a -> t). For a "wrapped" F t, we first convert it to Ff₁t * (t->t), and then "fmap" is defined exactly as in Ff₁t.

If we now create a value of Ff₂t using Wrap and then apply some "fmap" to it, we will get a value of the form

Wrap(F a) * (a -> t).

If we continue to apply "fmap" to this value, the part "Wrap(...)" will remain unchanged, just as in the case of Ff₁t.

However, now we can define "unwrap" that will distinguish between a value of Ff₁t which has just been constructed using "Wrap", and a value of type Ff₁t to which one or more "fmap"s have been applied. (The compiler might use this information to optimize the code.)

The price for this is relatively small: the type Ff₂t allows "nested" instances of Ffmap, such as
Ffmap ( Ffmap (...))
which cannot be a result of using Wrap or Fmap, but are nevertheless valid values of type Ff₂t. In other words, the same value of type Ff₂t can be encoded in many different and theoretically equivalent ways. This is a redundancy that, probably, does not actually affect any real-life applications of the free functor.

As we see, the definitions Ff₁t and Ff₂t are not fully equivalent; Ff₂t is a redundant encoding that in principle allows more optimization.

To get the best of Ff₁t and Ff₂t, we can retain Wrap but define the recursive case so that nested instances are not allowed:

data Ff₃ t where
Wrap :: F t -> Ff₃ t
Ffmap :: ∀a. F a * (a -> t) -> Ff₃ t

Now, Ff₃ t has two variants: one, Wrap, to which no "fmap" has been applied, and another, Ffmap, which is a result of applying fmap. The implementation of fmap will have to pattern-match on these two cases, converting a Wrap to an Ffmap.

-- Haskell
fmap (Wrap ft) = Ffmap ft id
fmap (Ffmap fa g)) h = Ffmap fa (h . g)
unwrap :: Ff₃ t -> Maybe (F t)
unwrap (Wrap ft) = Just ft
unwrap (Ffmap _ _) = Nothing

(to be continued)