Services
BiotechFintechAutonomous Vehicles
Open sourceContactCareersTeamResearchBlog
16 January 2020 — by Arnaud Spiwack
A Tale of Two Functors or: How I learned to Stop Worrying and Love Data and Control
haskelllinear-types

Haskell’s Data and Control module hierarchies have always bugged me. They feel arbitrary. There’s Data.Functor and Control.Monad—why? Monads are, after all, functors. They should belong to the same hierarchy!

I’m not that person anymore. Now, I understand that the intuition behind the Data/Control separation is rooted in a deep technical justification. But—you rightly insist—monads are still functors! So what’s happening here? Well, the truth is that there are two different kinds of functors. But you could never tell them apart because they coincide in regular Haskell.

But they are different—so let’s split them into two kinds: data functors and control functors. We can use linear-types to show why they are different. Let’s get started.

Data functors

If you haven’t read about linear types, you may want to check out Tweag’s other posts on the topic. Notwithstanding, here’s a quick summary: linear types introduce a new type a ⊸ b of linear functions. A linear function is a function that, roughly, uses its argument exactly once.

With that in mind, let’s consider a prototypical functor: lists.

instance Functor [] where
  fmap :: (a -> b) -> [a] -> [b]
  fmap f [] = []
  fmap f (a:l) = (f a) : (fmap f l)

How could we give it a linear type?

  • Surely, it’s ok to take a linear function as an argument (if fmap works on any function, it will work on functions which happen to be linear).
  • The f function is, on the other hand, not used linearly: it’s used once per element of a list (of which there can be many!). So the second arrow must be a regular arrow.
  • However, we are calling f on each element of the list exactly once. So it makes sense to make the rightmost arrow linear—exactly once.

So we get the following alternative type for list’s fmap:

fmap :: (ab) -> [a][b]

List is a functor because it is a container of data. It is a data functor.

class Data.Functor f where
  fmap :: (ab) -> f af b

Some data functors can be extended to applicatives:

class Data.Applicative f where
  pure :: a -> f a
  (<*>) :: f (ab)f af b

That means that containers of type f a can be zipped together. It also constrains the type of pure: I typically need more than one occurrence of my element to make a container that can be zipped with something else. Therefore pure can’t be linear.

As an example, vectors of size 2 are data applicatives:

data V2 a = V2 a a

instance Data.Functor f where
  fmap f (V2 x y) = V2 (f x) (f y)

instance Data.Applicative f where
  pure x = V2 x x
  (V2 f g) <*> (V2 x y) = V2 (f x) (g y)

Lists would almost work, too, but there is no linear way to zip together two lists of different sizes. Note: such an instance would correspond to the Applicative instance of ZipList in base, the Applicative instance for [], in base is definitely not linear (left as an exercise to the reader).

Control functors

The story takes an interesting turn when considering monads. There is only one reasonable type for a linear monadic bind:

(>>=) :: m a(am b)m b

Any other choice of linearization and you will either get no linear values at all (if the continuation is given type a -> m b), or you can’t use linear values anywhere (if the two other arrows are non-linear). In short: if you want the do-notation to work, you need monads to have this precise type.

Now, you may remember that, from (>>=) alone, it is possible to derive fmap:

fmap :: (ab)m am b
fmap f x = x >>= (\a -> return (f a))

But wait! Something happened here: all the arrows are linear! We’ve just discovered a new kind of functor! Rather than containing data, we see them as wrapping a result value with an effect. They are control functors.

class Control.Functor m where
  fmap :: (ab)m am b

class Control.Applicative m where
  pure :: am a  -- notice how pure is linear, but Data.pure wasn't
  (<*>) :: m (ab)m am b

class Control.Monad m where
  (>>=) :: (>>=) :: m a(am b)m b

Lists are not one of these. Why? Because you cannot map over a list with a single use of the function! (Neither is Maybe because you may drop the function altogether, which is not permitted either.)

The prototypical example of a control functor is linear State

newtype State s a = State (s(s, a))

instance Control.Functor (State s) where
  fmap f (State act) = \s -> on2 f (act s)
    where
      on2 :: (ab)(s, a)(s, b)
      on2 g (s, a) = (s, g b)

Conclusion

There you have it. There indeed are two kinds of functors: data and control.

  • Data functors are containers: they contain many values; some are data applicatives that let you zip containers together.
  • Control functors contain a single value and are all about effects; some are monads that the do-notation can chain.

That is all you need to know. Really.

But if you want to delve deeper, follow me to the next section because there is, actually, a solid mathematical foundation behind it all. It involves a branch of category theory called enriched category theory.

Either way, I hope you enjoyed the post and learned lots. Thanks for reading!

Appendix: The maths behind it all

Briefly, in a category, you have a collection of objects and sets of morphisms between them. Then, the game of category theory is to replace sets in some part of mathematics, by objects in some category. For example, one can substitute “set” in the definition of group by topological space (topological group) or by smooth manifold (Lie group).

Enriched category theory is about playing this game on the definition of categories itself: a category enriched in C\mathcal{C} has a collection of objects and objects-of-C\mathcal{C} of morphisms between them.

For instance, we can consider categories enriched in abelian groups: between each pair of objects there is an abelian group of morphisms. In particular, there is at least one morphism, 0, between each pair of objects. The category of vector spaces over a given field (and, more generally, of modules over a given ring) is enriched in abelian groups. Categories enriched in abelian groups are relevant, for instance, to homology theory.

There is a theorem that all symmetric monoidal closed categories (of which the category of abelian groups is an example) are enriched in themselves. Therefore, the category of abelian groups itself is another example of a category enriched in abelian groups. Crucially for us, the category of types and linear functions is also symmetric monoidal closed. Hence is enriched in itself!

Functors can either respect this enrichment (in which case we say that they are enriched functors) or not. In the category Hask (seen as a proxy for the category of sets), this theorem is just saying that all functors are enriched because “Set-enriched functor” means the same as “regular functor”. That’s why Haskell without linear types doesn’t need a separate enriched functor type class.

In the category of abelian groups, the functor which maps AA to AAA\otimes A is an example of a functor which is not enriched: the map from ABA → B to AABBA\otimes A → B\otimes B, which maps ff to fff\otimes f is not a group morphism. But the functor from AA to AAA\oplus A is.

Control functors are the enriched functors of the category of linear functions, while data functors are the regular functors.

Here’s the last bit of insight: why isn’t there a Data.Monad? The mathematical notion of a monad does apply perfectly well to data functors—it just wouldn’t be especially useful in Haskell. We need the monad to be strong for things like the do-notation to work correctly. But, as it happens, a strong functor is the same as an enriched functor, so data monads aren’t strong. Except in Hask, of course, where data monads and control monads, being the same, are, in particular, strong.

If you enjoyed this article, you might be interested in joining the Tweag team.
This article is licensed under a Creative Commons Attribution 4.0 International license.
Interested in working at Tweag?Join us
See our work
  • Biotech
  • Fintech
  • Autonomous vehicles
  • Open source
Tweag
Tweag HQ → 207 Rue de Bercy — 75012 Paris — France
hello@tweag.io
© Tweag I/O Limited. All rights reserved
Privacy Policy