Skip to Content »

Michi’s blog » Classifying spaces and Haskell

 Classifying spaces and Haskell

  • May 15th, 2014
  • 3:27 am

I’ve been talking with some topologists lately, and seen interesting constructions. I think these may potentially have some use in understanding Haskell or monads.

Simplicial objects

A simplicial object in a category is a collection of objects $C_n$ together with n maps $d_j:C_n\to C_{n-1}$ and n maps $s_j:C_n\to C_{n+1}$ subject to a particular collection of axioms.

The axioms are modeled on the prototypical simplicial structure: if $C_n$ is taken to be a (weakly) increasing list of integers, $d_j$ skips the $j$th entry, and $s_j$ repeats the $j$th entry. For the exact relations, I refer you to Wikipedia.

Classifying spaces

Take a category C. We can build a simplicial object $C_*$ from C by the following construction:

$C_n$ is all sequences $c_0\xrightarrow{f_0}c_1\xrightarrow{f_1}\dots\xrightarrow{f_{n-1}}c_n$ of composable morphisms in $C$.
$d_j$ composes the $j$th and $j+1$st morphisms. $d_0$ drops the first morphism and $d_n$ drops the last morphism.
$s_j$ inserts the identity map at the $j$th spot.

We can build a topological space from a simplicial object: dimension by dimension, we glue the product $\Delta^{n-1}\times C_n$ of an $n-1$-dimensional simplex and the object $C_n$ to the lower dimensional construction — with the face maps dictating the gluing step.

Classifying space of Hask

Consider the category of Haskell types and functions. The classifying space here will have an $n$-dimensional simplex for any sequence of $n+1$ composable functions; glued to the lower-dimensional simplices by composing adjacent functions.

I honestly am not entirely sure what structure, if any, can be found here: this might model $\beta$-reductions; or it might model something utterly trivial — I wonder what, if anything, can be found here, but I currently have no answers.

Classifying space of a Monad

We can do the same thing in the category of endofunctors. Recall that a Monad is an endofunctor $T$ with natural transformations $b:T^2\to T$ and $u:1\to T$. Just like any monoid, there is a category structure that fits in this framework. The simplicial object here is $T_*$ with $T_n=T^(n+1)$. The face maps $d_j$ compose two adjacent applications of $T$ using $b$. Degeneracy maps $s_j$ introduce a new $T$ by applying $u$.

For an example, let’s consider the Writer monad, for a monoid w:

newtype Writer w a = Writer { runWriter :: (a, w) }
return a = (a, mone)
bind ((a, w0), w1) = (a, w0 `mappend` w1)

The endofunctor here is Writer w :: * -> *. Iterating this endofunctor gets us (Writer w)^n a = (((...(a,w),w),w),w)...,w). A typical value would be something like

(((...(a,w0),w1),w2),...,wn) :: (Writer w)^n a

We get a simplicial structure here by letting the $j$th face map apply mappend to wj and w(j+1). The $j$th degeneracy map creates an instance of mone at the $j$th spot.

Let’s get more concrete. Consider Writer Any Bool. Recall that w0 `mappend` w1 = w0 `or` w1. For any value of of type x::a, there are $2^n$ values in (Writer w)^n a: one for each possible sequence of input to the Writer monad. Each of these produces an $n-1$-dimensional simplex, that glues to the lower dimensional simplices by fusing neighboring points.

In (Writer Any Bool)^0 there are two vertices: (x,False) and (x,True).

In (Writer Any Bool)^1 there are four edges: (x,True, True), (x,True, False), (x,False, True) and (x,False, False).
These connect to the vertices like this:
writer1 (1)

In (Writer Any Bool)^2 there are eight triangles. They glue as follows — each triangle gets its three edges in order:
FFF to FF, FF, FF
FFT to FT, FT, FT
FTF to TF, TF, FT
FTT to TT, TT, FT
TFF to FF, TF, TF
TFT to FT, TT, TT
TTF to TF, TF, TT
TTT to TT, TT, TT

It continues like this as we add higher and higher dimensional faces. Any history of $n$ writes to the monad produces an $n-1$-dimensional object, that connects to lower dimensions by looking at how the history could have been contracted by the monoid action at various points.

For the monad Writer All Bool, the same vertices, edges, triangles, et.c. show up, but they connect differently:
FF to F, F
FT to T, F
TF to F, F
TT to T, T
FFF to FF, FF, FF
FFT to FT, FT, FF
FTF to TF, FF, FF
FTT to TT, FT, FT
TFF to FF, FF, TF
TFT to FT, FT, TF
TTF to TF, TF, TF
TTT to TT, TT, TT

What can we use this for?

And here, at last, is my reason for writing all this. This construction gets us a topological space, where cells in the space (possibly even points in the space) correspond to possible values of the iterated monad datatype, and where connectivity in the space is driven by the monad. This gives us a geometric, a topological, handle on the programming language structure.

Is this good for anything?
Are there any sort of questions we might be able to approach with this sort of perspective?
I’ll be thinking about it, but if anyone out there has any sort of idea I’d love to hear from you.

Want your say?

* Required fields. Your e-mail address will not be published on this site

You can use the following XHTML tags:
<a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>