Sunday, October 13, 2019

Summary: You can describe type classes like monads by the graphs they allow.

In the Build Systems a la Carte paper we described build systems in terms of the type class their dependencies could take. This post takes the other view point - trying to describe type classes (e.g. `Functor`, `Applicative`, `Monad`) by the graphs they permit.

Functor

The `Functor` class has one operation: given `Functor m`, we have `fmap :: (a -> b) -> m a -> m b`. Consequently, if we want to end up with an `m b`, we need to start with an `m a` and apply `fmap` to it, and can repeatedly apply multiple `fmap` calls. The kind of graph that produces looks like:

We've used circles for the values `m a`/`m b` etc and lines to represent the `fmap` that connects them. `Functor` supplies no operations to "merge" two circles, so our dependencies form a linear tree. Thinking as a build system, this represents Docker, where base images can be extended to form new images (ignoring the newer multi-stage builds).

Applicative

The `Applicative` class has two fundamental operations - `pure :: a -> m a` (which we ignore because its pretty simple) and `liftA2 :: (a -> b -> c) -> m a -> m b -> m c` (most people think of `<*>` as the other fundamental operation, but `liftA2` is equivalent in power). Thinking from a graph perspective, we now have the ability to create a graph node that points at two children, and uses the function argument to `liftA2` to merge them. Since `Applicative` is a superset of `Functor`, we still have the ability to point at one child if we want. Children can also be pointed at by multiple parents, which just corresponds to reusing a value. We can visualise that with:

The structure of an `Applicative` graph can be calculated before any values on the graph have been calculated, which can be more efficient for tasks like parsing or build systems. When viewed as a build system, this represents build systems like Make (ignoring dependencies on generated Makefiles) or Buck, where all dependencies are given up front.

Selective

The next type class we look at is `Selective`, which can be characterised by the operation `ifS :: m Bool -> m a -> m a -> m a`. From a graph perspective, `Selective` interrogates the value of the first node, and then selects either the second or third node. We can visualise that as:

We use two arrows with arrow heads to indicate that we must point at one of the nodes, but don't know which. Unlike before, we don't know exactly what the final graph structure will be until we have computed the value on the first node of `ifS`. However, we can statically over-approximate the graph by assuming both branches will be taken. In build system terms, this graph corresponds to something like Dune.

The final type class is `Monad` which can be characterised with the operation `(>>=) :: m a -> (a -> m b) -> m b`. From a graph perspective, `Monad` interrogates the value of the first node, and then does whatever it likes to produce a second node. It can point at some existing node, or create a brand new node using the information from the first. We can visualise that as:

The use of an arrow pointing nowhere seems a bit odd, but it represents the unlimited options that the `Monad` provides. Before we always knew all the possible structures of the graph in advance. Now we can't know anything beyond a monad-node at all. As a build system, this graph represents a system like Shake.

Ondra said...

I know this is not the point of this post, but the Functor class graph _can_ be a tree: if I have `m a` and `a -> b`, I can create `m b`; but if I also have `a -> c`, I can also create `m c` from that. Something like

m a
/ \
/ \
m b m c

Also, it seems to me that it broadly aligns with the formal hierarchy of languages, where correspond

(1) regular languages/grammars ≈ finite state automata ≈ regular expressions ≈ linear/string-like graphs

(2) context-free languages/grammars ≈ pushdown automata ≈ μ-regular expressions ≈ tree graphs, and also Functor according to this blogpost

(3) context-sensitive languages/grammars ≈ linear bounded automaton (≈ simply-typed lambda calculus, I guess???) ≈ directed acyclic graphs, and also Applicative according to this blogpost

(4) recursively enumerable languages/unrestricted grammars ≈ Turing machine ≈ untyped lambda calculus ≈ any graph

Question is, what would be the Type Class for (1)? And is Monad the right Type Class for (4) or should there be something different?

Ondra said...

aww, blogger.com formating broke my beautiful graph :D but I hope you see what I mean

anyway, thank you very much for this thought-provoking post!

Neil Mitchell said...

Thanks for the comments Ondra, very interesting. You can make a tree of functors of type m a, but for any particular value m a, it can only be generated in one way. Interesting connection to the hierarchy of languages, would be great to see a formal treatment of that - it seems about right, but I'd love to know what lemma shows the correspondence.

Christopher Done said...

Is the graph for Applicative really accurate? (https://3.bp.blogspot.com/-A8fyuxlE3qQ/XaOD_u7DMkI/AAAAAAAABe4/ePXkqtOqRkMt_D6DpYUWw8dKkzS0VwZFgCLcBGAsYHQ/s1600/Applicative.png)

How would you write that graph with Applicative class's methods?