A pedestrian introduction to Monad and Guix

First thing first, launch guix repl to run the code snippets. We will extensively use pattern matching, thus I recommend to give a look at the examples from Guile documentation. That’s said, go.

Let naively implement a nap function (normally called map) applying a function f to the list lst.

(use-modules (ice-9 match))

(define (nap f lst)
  (match lst
    ((x xs ...)
     (cons (f x) (nap f xs)))
    (_ '())))

If two functions have type-signature compatibility, then one can easily compose them,

(define (g x) (string->number x))
(define (h x) (* x x))
(nap (compose h g) (list "1" "2" "3"))
;; <->
(nap h (nap g (list "1" "2" "3")))

The flow reads from right to left; though using infix notation we should read: the data (list "1" "2" "3") flow via g flow via h. In short, the two ingredients to make the composition working are:

• match which somehow unwraps (or unpacks),
• cons which somehow wraps back (or packs).

So far, so good. Now, consider the repeat function which takes a seed and generates a list,

(define (repeat seed) (list seed seed))
(repeat "hello") ;; => ("hello" "hello")

and we would like to compute the result ("hello" "hello" "hello" "hello" "world" "world" "world" "world") from the input (list "hello" "world"). In other words, we would like someting able to compose repeat. If repeat is composed to itself using compose as previously, then the result is (("hello" "hello") ("hello" "hello")); not what we want. We want a simple list back. Therefore concatenate from SRFI-1 seems the thing we need.

(use-modules (srfi srfi-1))

(define (bind-list f lst)
  (concatenate (nap f lst)))

(bind-list repeat (bind-list repeat (list "hello" "world")))
;; => ("hello" "hello" "hello" "hello" "world" "world" "world" "world")

Wow! First, please note the same pattern as composing previously with nap. Reading right to left with infix notation: the list data bind to repeat bind to repeat. Second, bind-list somehow acts as an unwrap-rewrapper. What could somehow acts as a wrapper? Pick the simplest:

(define (return-list x)
  (list x))

Attentive reader might notice nice properties between bind-list and return-list; it is let as an exercise to verify¹ all these instances:

(bind-list repeat (return-list "one"))   ;; (repeat "one")
(bind-list return-list (list "two"))     ;; (list "two")

(bind-list repeat (bind-list repeat (list "three")))
;; eq?
(bind-list
 (lambda (x) (bind-list repeat (repeat x)))
 (list "three"))

Do you still follow? If yes, congrat! Because we just have defined the list monad. The terms bind and return are the common names for these unwrap-rewrapper and wrapper. Not convinced yet by the concept, let jump into another example.

Let consider a tiny calculator. The example is borrowed from Graham Hutton at Computerphile . We start with expressions and a recursive evaluator. Here we oversimplify the underlying datatype to stay on track and thus avoid the introduction of unrelated Guile concepts. An expression is represented by a nested sequence of “nodes” (neg, add, div) where the “leaf” is represented by val with an associated value.

(define expr '(add (val 1) (neg (val 1))))
(define bang  `(div (val 1) ,expr))

(define (evaluator e)
  (match e
    (('val x) x)
    (('neg x) (- 0 (evaluator x)))
    (('add e1 e2) (+ (evaluator e1) (evaluator e2)))
    (('div e1 e2) (/ (evaluator e1) (evaluator e2)))))

The evaluator walks the sequence and last return a value (number). Nothing fancy. The well-known issue is the division by zero. For instance, (evaluator bang) throws the error ("/" "Numerical overflow" #f #f)'. The question is thus: how to prevent this error? One solution is to define a datatype and a function catching the potential error. Let write it,

(define (safe-div n m)
  (match m
    ((? = 0) 'nothing)
    (_ `(just ,(/ n m)))))

This function now returns maybe the result: if the division makes sense, then it just returns it, else it returns nothing. So far, so good.

However, now this function safe-div cannot be composed with usual other arithmetic operations; for instance, (+ 1 (safe-div 4 2)) does not make sense at the type level. Somehow, we need a way to unwrap the value. The evaluator has to be adjusted accordingly, i.e., it cannot return a number anymore; instead it has to return either nothing (something went wrong) or either (just number) (the computation is just that).

(define (evaluator-bis e)
  (match e
    (('val x) `(just ,x))
    (('neg x)
     (match (evaluator-bis x)
       ('nothing 'nothing)
       (('just y) `(just ,(- 0 y)))))
    (('add e1 e2)
     (match (evaluator-bis e1)
       ('nothing 'nothing)
       (('just x1)
        (match (evaluator-bis e2)
          ('nothing 'nothing)
          (('just x2) `(just ,(+ x1 x2)))))))
    (('div e1 e2)
     (match (evaluator-bis e1)
       ('nothing 'nothing)
       (('just x1)
        (match (evaluator-bis e2)
          ('nothing 'nothing)
          (('just x2) (safe-div x1 x2))))))))

Here we are, (evaluator-bis bang) returns now nothing. Wait! Are we seeing again some unwrapper-wrapper? Attentive reader might notice that, first, a pattern emerges, isn’t it? And second, the issue is about composition, right? We already know what is the next step. Let’s go define this pattern and re-write the evaluator.

(define (bind-maybe f m)
  (match m
    ('nothing 'nothing)
    (('just x) (f x))))

(define (return-maybe x)
  `(just ,x))

(define (safe-evaluator e)
  (match e
    (('val x) (return-maybe x))
    (('neg x)
     (bind-maybe
      (lambda (y) (return-maybe (- 0 y)))
      (safe-evaluator x)))
    (('add e1 e2)
     (bind-maybe (lambda (x1)
        (bind-maybe (lambda (x2)
                      (return-maybe (+ x1 x2)))
                    (safe-evaluator e2)))
                 (safe-evaluator e1)))
    (('div e1 e2)
     (bind-maybe (lambda (x1)
        (bind-maybe (lambda (x2)
                      (safe-div x1 x2))
                    (safe-evaluator e2)))
                 (safe-evaluator e1)))))

This safe-evaluator is better because it only depends on how the datatype of an expression is represented. The internal representation of an impossible computation is captured by another datatype; this other datatype could capture more information about the context than the computation itself. The main point is to be still able to compose, i.e., unwrap-rewrap transparently without worrying about the structure of the richer datatype. It is tempting to add syntactic sugar and abstract the remaining pattern; let as an exercise. Again, attentive reader might notice these identities:

(define (f x) (if (< x 0) 'nothing `(just ,x)))

(bind-maybe f (return-maybe 1))         ; (f 1)  ;; => (just 1)
(bind-maybe f (return-maybe -1))        ; (f -1) ;; => nothing

(bind-maybe return-maybe '(just 2))     ; => (just 2)
(bind-maybe return-maybe '(just -2))    ; => (just -2)

(bind-maybe f (bind-maybe f '(just 3)))
;; eq? => (just 3)
(bind-maybe
 (lambda (x) (bind-maybe f (f x)))
 '(just 3))

(bind-maybe f (bind-maybe f '(just -3)))
;; eq? => nothing
(bind-maybe
 (lambda (x) (bind-maybe f (f x)))
 '(just -3))

Oh, are we speaking about the maybe monad? Yes! The monad concept is not so complicated after all, isn’t it?

A monad is a mathematical object composed by:

1. a type constructor,
2. a function return,
3. a function bind.

Considering a type a, the monadic type reads m a. For instance, the type a means number and m means list; or number and “ maybe ”. The signature is: return :: a \(\rightarrow\) m a; from a value of type a is returned a monadic value of type m a. The function bind is less intuitive; the signature² is:

which means bind takes first a function which takes a normal value and returns a monadic value (value with context) and second a monadic value, then this bind returns a monadic value (value with context). Well, I hope that framing these words with the above example using the maybe monad helps, maybe.

Somehow, a monad encapsulates an object to another object owning more information. And the two associated functions provide the composition.

These two functions return and bind are not randomly picked. They also must respect the three laws to fully qualify as a monad:

1. return is a left-identity for bind,
2. return is a right-identity for bind,
3. bind is associative.

The test suite of Guix checks these three laws (for specific monad). They are strong invariant properties but attached to concrete types. In other words, the term monad refers to a generic mathematical object defined by 3+3 items, then attached to specific types, i.e., once defined concrete constructor, return and bind, one can define specific monads as the list monad, maybe monad and many more as the state monad.

To end, let challenge our parser: these three laws formally written read,

where bind is usually denoted >>= flipping the argument order and with an infix notation: \(x~\texttt{>>=}~f\) means \((\texttt{>>=}~x~f) = (\texttt{bind}~f~x)\), therefore the three laws now read³,

Don’t fear the monad!

Monad provides a framework to compose effects (or context) under control (or purity). In Guix terminology, these effects are the various states (profiles, generations, etc.) kept under control by using isolated environments. Functional package management⁴ sees the package definition (recipe) as a pure mathematical function \(\texttt{a}~\rightarrow~\texttt{b}\) but that alone is useless for practical purposes. Build a package could somehow be seen as a function \(\texttt{a}~\rightarrow~\texttt{m b}\) where m is a controlled context. However, compose such functions, e.g., build a profile, is not straightforward as we have shown by tiny examples. What Guix calls the store monad is the framework to make functional package management useful and safe; at least an attempt.

Reader, if you are still there, I recommend you three extensive presentations:

• give a look at Category theory for Scientists by David Spivak who exposes bottom-up the material targeting broader scientific community;
• Category theory for Programmers by Bartosz Milewski who deeply introduces core concepts targeting programmers;
• a bit aged but still classic Categories for the Working Mathematician by Saunders Mac Lane who provides mathematical details for people with a strong background about abstraction.

Although I have never fully completed all these materials. :-)