This post will discuss how to model Simplicial Sets (sSets) in Haskell, using their category-theoretic definition.
If you want to know what these are, a good primer is Friedman's introduction to simplicial sets. Another, more concrete perspective is provided by Sergeraert's introduction to combinatorial homotopy theory
Now why would we want to model this thing anyway, and why are we going to jump through categorical hoops to do so?
Well, we want to model sSets because they are a basic way in which people carry out homotopy theory, which in turn is about reducing the class of spaces (or shapes, if you prefer) into spaces modulo their continuous transformations into one another, thus giving us a way to talk about shapes/spaces ""in general"". Now in turn we need to represent shapes/spaces in a concrete way, and we do so by identifying them with certain decompositions of them into more basic things that we can count and represent explicitly, etc. So this is in fact a very ""computer sciencey"" type of problem -- that of finding a data structure that captures the information we're interested in and nothing else.
One particular point of interest is that there is a model of type theory given by a translation to sSets. This model, produced by Voevodsky, exhibits the important property that a principle called ""univalence"" holds, which is roughly translated as ""equivalence is equivalent to equality."" This makes precise the notion that if two structures are in bijection, then they are for all practical purposes, the same thing.
sSets are weird creatures however, and not especially suited to direct respresentation. In a typically mathy fashion, they constitute a very general collection of data and relations subject to many constraints on how the relations and data interact. So it is doubly ""computer sciency"" to want to find a structure that captures an sSet itself in such a way that all the relations necessarily obey all the constraints we want.
And here the category theoretic representation of sSets comes into play. Properly defined, all the things that constitute an sSet ""fall out"" of their category theoretic representation directly, and so if we define sSets as directly given from their category theoretic description, then the ""size"" of our model and structure should match. Furthermore, the category theoretic description is itself built out of smaller components, so we can build things up incrementally, and observe a topological/combinatorial strucuture appear as if my magic at the last step.
Since the category theory involved, while not complicated, is also nontrivial, this also serves as an exercise in learning how to directly encode category theory in haskell, as opposed to the usual constructions which are really all in terms of endofunctors on Hask.
Nearly all of what follows is borrowed directly from Sjoerd Visscher's data-category library, which is pretty darn neat. Thanks to rwbarton and shachaf for talking me through this on IRC.
So first we introduce categories. Recall that objects are considered to have no internal structure, so there is only ""one"" of each object in any given category. Arrows between objects, however, are collected as elements of Set (or, in our case, Hask), and so there can be many morphisms between any two objects in a category (or no morphisms). Hence we represent objects simply as types, and morphisms as values. If we ever need to refer to an object directly as a value, we equate it with the identity arrow to itself. This has the additional advantage that since ""arrows come first"" and we can only ""create"" objects from arrows, if we cannot create an arrow with a given domain or codomain, we cannot treat that type as a member of our category. (Contrast this with the approach in the standard Category typeclass, where all types in Hask are the member of every category thus created, since the typeclass equips them all with an identity arrow directly.)
type Obj k a = k a a
class Category k where
src :: k a b -> Obj k a
tgt :: k a b -> Obj k b
o :: k b c -> k a b -> k a cThe basic category that we'll use to take the place of Set in our constructions is Hask, and we can easily equip it as in instance of our provided Category class, with composition and identity functions defined the obvious way:
instance Category (->) where
src _ = id
tgt _ = id
f . g = f . gNext up, we want to introduce a certain category known as the Simplex Category. This category is often denoted by the Delta symbol (Δ), or the delta symbol with an underscore, or the delta symbol with a hat, depending on convention. This category is described pretty succintly in Sergeraert, section 3.1 and Friedman, definition 2.9. Here's my stab at it, as concretely as possible
Objects of Δ are the sets {1}, {1,2}, {1,2,3}, etc. That is to say, they are nonempty, ordered, and of a given size. We name these [1], [2], [3], etc. The morphisms in Δ are nondecreasing maps. That is to say, if we have a morphism [3] -> [4], we can think of it as composed as a list of 3 values, ranging between 1 and 4, with the property that this list is nondecreasing. |1,1,1| for example, sends every element in [3] to the value 1 in [4]. |1,2,3| is the ""injective identity"" (so to speak), and |2,1,1| is not allowed. We can also envision this by putting three dots in a vertical line, and four dots in another vertical line, like so:
.
. .
. .
. .
Now we draw an arrow from every dot on the lefthand side to one on the righthand side, such that the arrows do not cross. Such a diagram also corresponds to a morphism.
If we start to enumerate our morphisms, a familiar pattern emerges. For any [n]=>[1] we have only one unique morphism. That is to say that [1] is the terminal object of this category. Conversely, [1] => [n] always has [n] morphisms, one for each element of [n]. Meanwhile, consider an arbitrary [n] => [m] for n and m both greater than one. We can think of it as decomposing completely into the relation (1,1) augmenting all relations between [n-1] => [m] or all relations that do not target 1 on the right hand side at all -- i.e. the same count as [n] -> [m - 1].
This is to say, draw a line between the bottom two dots. Now what you have one less dot on the left hand side, but otherwise the same picture (in terms of what lines you can draw next). Now if you say that there is not a line between the bottom two dots, then therefore no line goes to the bottom right dot.
We can write this out in a grid, like so.
| | 1 | 2 | 3 | 4 | 5 |
| - | - | - | - | - | - |
| 1 | 1 | 2 | 3 | 4 | 5 |
| 2 | 1 | 3 | 6 | 10 | 15 |
| 3 | 1 | 4 | 10 | 20 | 35 |
| 4 | 1 | 5 | 15 | 35 | 70 |
Eagle-eyed readers will recognize a familiar pattern -- this is a 45 degree rotation of Pascal's Triangle! Here, each entry aside from the ones in initial row and column can be determined by summing the entry above it and the entry to its right.
This in turn suggests something neat from the Haskell standpoint. The count of morphisms between any two objects is inductively defined. Thus, we should be able to create these morphisms from an inductively defined datatype.
Let's write the following, representing our objects as the standard collection of Peano numerals (starting at One rather than Zero)
data O
data S n
data Delta a b where
MorphZero :: Delta O O
SuccSrc :: Delta a b -> Delta (S a) b
SuccTgt :: Delta a b -> Delta a (S b)
-- | Given any object in Delta, find the successor.
succObj :: Obj Delta n -> Obj Delta (S n)
succObj = SuccSrc . SuccTgt
instance Category Delta where
src MorphZero = MorphZero
src (SuccSrc f) = succObj (src f)
src (SuccTgt f) = src f
tgt MorphZero = MorphZero
tgt (SuccSrc f) = tgt x
tgt (SuccTgt f) = succObj (tgt f)
o MorphZero f = f
o f MorphZero = f
o (SuccTgt f) g = SuccTgt (f `o` g)
o f (SuccSrc g) = SuccSrc (f `o` g)
o (SuccSrc f) (SuccTgt g) = f `o` g
The source and target definitions are pretty straightforward. In each case we have a base case of MorphZero and apply the succObj operation precisely as many times as the data type has incremented either the source or target, respectively.
Composition is somewhat more subtle. Composition with the unit morphism changes nothing. Postcomposing something with an incremented target is the same as incrementing the target of the underlying composition; i.e. b->(S c) . a->b is morally (SuccTgt (b->c . a->b)). Ditto precomposing something with an incremented source, where we map b->c . (S a)->b to SuccSrc (b->c . a->b). And in the case where the src and target are incremented such that we have something like (Succ b)->c . a->(Succ b), we can equate this with b->c . a->b. This ""diagonal"" path feel like it throws away information. But that information about other possible paths is in fact held in the other two, far more common cases.
Here we will now introduce a few simple utility functions for actually displaying and creating objects of Delta, just so we can start to play with it more directly.
deltaToInt :: Obj Delta n -> Int
deltaToInt MorphZero = 0
deltaToInt (SuccSrc (SuccTgt d)) = 1 + deltaToInt d
deltaToInt x = deltaToInt (src x)
showDelta :: Obj Delta n -> String
showDelta = show . deltaToInt
zero = MorphZero
one = succObj zero
two = succObj one
three = succObj twoBut this Delta category was only the first step. We really want its opposite category. With this representation, introducing opposite categories is luckily virtually textbook, just quite literally swapping the direction of all arrows.
data Op k a b = Op { unOp :: k b a }
-- | @Op k@ is opposite category of the category @k@.
instance Category k => Category (Op k) where
src (Op a) = Op (tgt a)
tgt (Op a) = Op (src a)
o (Op a) (Op b) = Op (b `o` a)Even this doesn't take us very far. We are interested not in the Delta category itself, nor in its opposite category, but in functors from Δ^op -> Set. In general, functors whose codomain is in Set are called ""presheaves"" and for some category C, a functor C^op -> Set is called a (set valued) ""presheaf on C"".
So do characterize this, we need to talk about categories themselves as objects, and functors between them as morphisms in the category Cat.
First introduce morphisms in the category Cat as such:
class (Category (Dom f), Category (Cod f)) => CFunctor f where
type Dom f :: * -> * -> *
type Cod f :: * -> * -> *
type MapObj f a :: *
mapArrow :: f -> Dom f a b -> Cod f (MapObj f a) (MapObj f b)
Dom extracts the type of the source category, Cod the target category. mapObj is the type that sends an object (represented as a type) across the functor to an object represented as a type of the target category. mapArrow is the function that given a functor, sends an arrow on two objects of the domain to the resulting arrow in the target category on two objects of the target domain.
Now if we make any type an instance of CFunctor we can say that it represents fully a mapping between two categories. (Of course we must enforce that it respects associated identity and composition laws, etc.)
One simple such functor for any category is the identity functor that sends it to itself, the obvious way.
data Id (k :: * -> * -> *) = Id
instance Category k => CFunctor (Id k) where
type Dom (Id k) = k
type Cod (Id k) = k
type MapObj k a = a
mapArrow _ f = fFurthermore, if we have two functors, such that the source of one matches the target of the other, we can compose them directly, and still have a functor.
data (g :.: h) where
(:.:) :: (CFunctor g, CFunctor h, Cod h ~ Dom g) => g -> h -> g :.: h
instance (Category (Dom h), Category (Cod h), Category (Dom g), Category (Cod g)) => CFunctor (g :.: h) where
type Dom (g :.: h) = Dom h
type Cod (g :.: h) = Cod g
type MapObj (g :.: h) a = MapObj g (MapObj h a)
mapArrow (g :.: h) = mapArrow g . mapArrow hNow we need a way of wrapping up a type constructor of arity two (i.e. the morphism type of some category, in our formulation) as an object itself.
We introduce
data CatCon :: (* -> * -> *) -> *This just wraps up a type constructor so we may treat it as a full type. Note that the data type has no constructors, and we only use this at the type level.
Now that we can represent the type of objects of Cat and the character of arrows of Cat, we can write the concrete type of arrows in the category Cat.
data Cat j k where
CatA :: (CFunctor f) => f -> Cat (CatCon (Dom f)) (CatCon (Cod f))This says that if f is a functor, then we can wrap it up as a concrete morphism in the category Cat that maps between its domain and codomain, themselves treated as objects.
This lets us finally give the Category instance for the category of categories ""Cat"".
instance Category Cat where
src (CatA _) = CatA Id
tgt (CatA _) = CatA Id
o (CatA f) (CatA g) = CatA (f :.: g)In our constructions, Hask takes the place of Set. So we must not only have the category Delta, but the category Hask, as given above. Now, finally, we can define the class of morphisms that send Delta^Op to Hask.
type SSetSimple = Cat (Op Delta) (->)But that's just a type! How do we produce such a creature? There are many possible mappings between these two categories, and we can't even create a data type that encompasses them all, as different mappings may not just produce different concrete arrows, but different correspondences between types. As we see, we will need to construct a slightly stronger type that holds more information to really work with such objects.
We can start with characterizing one special collection of SSet -- those that are embeddings of Delta into the functor category Delta^Op -> Set -- i.e. those coming directly from the Yoneda embedding. Since the Yoneda construction is slightly intricate, it is worth a brief digression to introduce it.
The Yoneda embedding in fact maps objects themselves into functors, so we'll start by describing the sorts of functors it maps objects into.
We begin with the contravariant Hom functor. This says that for each object X in delta, (in our case types like Z, S Z, etc.), we want a functor that sends objects in Delta (again, types like Z, S Z, etc.) to objects in the homset that characterize arrows into X. So in our case this is types like Delta a X, and what we want, in pure Haskell notation, is a type of the form Obj Delta a -> (Obj Delta b -> (Delta b a)). What about mapping morphism to morphisms? Well, here we first take the object again, but we use it to produce a map on morphisms instead. So we get a value of the form Obj Delta c -> (Delta a b -> (Delta b c -> Delta a c)). We can now write down a general creature that gives us our contravariant Hom functor on any category, with mapping arrows given as precomposition.
data ContraHom k a where
ContraHom :: Obj k a -> ContraHom k a
instance Category k => CFunctor (ContraHom k a) where
type Dom (ContraHom k a) = (Op k)
type Cod (ContraHom k a) = (->)
type MapObj (ContraHom k a) b = k b a
-- X is unused because it _just_ witnesses the existance of an object in K.
mapArrow (ContraHom x) (Op f) = \g -> g `o` f
Now we can wish to treat these ContraHom functors themselves as objects of a category. But ""arrows first,"" we must define what morphisms on these functors are. The answer is that morphisms between presheaves are natural transformations between them, sending objects in our source category to contravariant morphisms in our target category, satisfying coherence conditions.
data Presheaves k f g where
NTrans :: (CFunctor f, CFunctor g, k ~ Dom f, k ~ Dom g, (->) ~ Cod g, (->) ~ Cod f) => f -> g -> (forall z. k z z -> (MapObj f z) -> (MapObj g z)) -> Presheaves k f g
pshId :: (CFunctor f, (->) ~ Cod f) => f -> Presheaves (Dom f) f f
pshId f = NTrans f f (\i -> mapArrow f i)
instance Category k => Category (Presheaves k) where
src (NTrans f _ _) = pshId f
tgt (NTrans _ g _) = pshId g
o (NTrans _ h ngh) (NTrans f _ nfg) = NTrans f h (\i -> ngh i . nfg i)
The above definition is somewhat ""bigger"" than what we want, in that it does not enforce coherence conditions, but this is to be expected in haskell. Additionally, we have defined covariant presheaves, rather than the more typical contravariant one. So if we want a contravariant presheaf, we simply need to apply the ""Op"" constructor explicitly ourselves -- which isn't so bad, since it lets us keep track, more explicitly, of where our variances swap back and forth, which I have found is the greatest difficulty in building these constructions.
Now we are prepared to give the Yoneda Lemma as applied to this embedding. This lemma says that natural transformations between any two presheaves given by the hom functor on our source category are in one to one correspondence, contravariantly, to the arrows in the source category.
That is to say we have the following function that embeds morphisms in our source category into morphisms in the presheaf category over it.
arrToPsh :: Category k => k a b -> Presheaves (Op k) (ContraHom k a) (ContraHom k b)
arrToPsh arr = NTrans (ContraHom $ src arr) (ContraHom $ tgt arr) $ \_ -> \j -> arr `o` j
The Yoneda Embedding itself can be stated as a functor.
type YonedaPsh k a b = Presheaves k (ContraHom k a) (ContraHom k b)
data PshFunctor k
instance Category k => CFunctor (PshFunctor (CatCon k)) where
type Dom (PshFunctor (CatCon k)) = k
type Cod (PshFunctor (CatCon k)) = Presheaves (Op k)
type MapObj (PshFunctor (CatCon k)) a = ContraHom k a
mapArrow _ = arrToPshAnd the Yoneda Lemma applied to this functor is the statement that it is full and faithful. This is to say that objects in our source category have corresponding objects in our target category, and furthermore that of those ""representable"" objects in our target category (i.e. ones which come from our source category), then the arrows between them are in complete correspondence to the arrows between the represented objects in the source category.
Now, finally, we have a proper, rich enough type to characterize simplical sets we can work with.
type SSet = Presheaves (Op Delta)This post leaves off where the going gets a bit hard and interesting. How do we build interesting inhabitants of this type? Can we encode realization as a functor, and describe probing these presheaves? Given the "representable" ones, how can we build a colimit construction such that we can produce the rest of them? For now, I leave that to you.