Sunday, October 13, 2019

Monads as Graphs

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.

Monad

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.

5 comments:

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?

I wrote up my view with diagrams here: https://www.reddit.com/r/haskell/comments/djfsyq/monads_as_graphs_and_a_relationship_to_the/f45rbi5/

Wasn't sure how to do it in blogger.com's formatting.

Neil Mitchell said...

@Christopher: There are two possible ways. You can either encode the graph like https://www.reddit.com/r/haskell/comments/djfsyq/monads_as_graphs_and_a_relationship_to_the/f49qmrp, or assume that things are deduplicated at some other layer (as all build systems actually do).

If you take your approach, then you would have to draw a tree with no sharing for Applicative, which isn't unreasonable, but that strongly suggests there is a type class that has sharing but no other powers. Keen to see what that type class looks like.