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:
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.