I recently found a way to represent sheaves in Haskell. It was a fun couple of weeks of head-scratching. But as much as I wanted it to, the code in my demonstration repo doesn’t speak for itself. So I’m writing this blog post to share my newfound understanding. In this post I’ll be assuming a pretty solid knowledge of category theory (but not of sheaves, which I’ll be explaining). If you aren’t, wait until my next post which will give a more practical introduction to sheaves.

I don’t think it’s necessary to use Haskell for this. Other functional programming languages should work as well, but Haskell certainly makes some things easier as types get a bit dependent eventually. Of course, it would be even easier in a true dependently typed language, but the whole point was to avoid needing that level of sophistication.

As a general warning: all of this is about translating well-known mathematical concepts into Haskell. While doing so, I have to use a lot of approximations, as Haskell doesn’t have, say, a notion of equality. I will generally not even mention any conditions that I’m supposed to prove to properly align with the mathematical definitions, and only focus on the operational aspects. I’ll try to leave enough breadcrumbs to fill in the gaps for those of you who would want to.

First, presheaves

I’ll start by giving a concrete instance of sheaves, which makes the definition surprisingly transparent. Later I’ll be expanding that to the general notion of sheaves.

Let’s give ourselves a category of arithmetic expressions, or rather, arithmetic functions. It’s got just enough material to illustrate the point.

type Ty :: Type
data Ty = TInt | TBool | TUnit | TProd Ty Ty

type Expr :: Ty -> Ty -> Type
data Expr i j where
  Id :: Expr i i
  Add :: Expr i TInt -> Expr i TInt -> Expr i TInt
  Sub :: Expr i TInt -> Expr i TInt -> Expr i TInt
  Mult :: Expr i TInt -> Expr i TInt -> Expr i TInt
  Unit :: Expr i TUnit
  IsZero :: Expr i TInt -> Expr i TBool
  IfThenElse :: Expr i TBool -> Expr i j -> Expr i j -> Expr i j

compose :: Expr i j -> Expr j k -> Expr i k
compose e Id = e
compose e (Add l r) = Add (compose e l) (compose e r)
compose e (Sub l r) = Sub (compose e l) (compose e r)
compose e (Mult l r) = Mult (compose e l) (compose e r)
compose e (IsZero n) = IsZero (compose e n)
compose e Unit = Unit
compose e (IfThenElse b t f) = IfThenElse (compose e b) (compose e t) (compose e f)

Now, consider the category of presheaves over Expr:

type Presheaf :: (Ty -> Type) -> Constraint
class Presheaf p where
  pb :: forall i j. Expr i j -> p j -> p i

(I named the presheaves’ restriction pb, for “pullback”, because we’re going to be writing it quite a lot.)

The category of presheaves (with natural transformations forall i. p i -> q i as morphisms) is a Cartesian closed category (and then some) which contains the Expr category as a full subcategory, via the Yoneda embedding

type Y :: Ty -> (Ty -> Type)
newtype Y j i = MkY (Expr i j)

instance Presheaf (Y i) where
  pb f (MkY g) = MkY (g `compose` f)

Therefore we can think of the category of presheaves as a completion of Expr with a bunch of extra structure. And the problem that we will want to solve is that presheaves actually add too much structure. This manifests in the impossibility of interpreting IfThenElse. Or, rather, the Yoneda embedding lets us build a presheaf

ifThenElse :: Y TBool i -> Y j i -> Y j i -> Y j i

But this isn’t the usual type of ifThenElse, we want instead

ifThenElse :: (Presheaf p) => forall i. Y Bool i -> p i -> p i -> p i

Sheaves, concretely

Unfortunately, we can’t define such an ifThenElse function. This is because Y TBool isn’t a coproduct in the category of presheaves. Presheaves create coproducts (and in fact all colimits) freely.

What we can do, however, is define a new type class, and we can even define it in the most on-the-nose way possible (because nobody is stopping us).

class Presheaf p => Sheaf p where
  glueIfThenElse :: forall i. Expr i TBool -> p i -> p i -> p i

ifThenElse :: Sheaf p => forall i. Y TBool i -> p i -> p i -> p i
ifThenElse (MkY e) = glueIfThenElse e

This is almost insultingly straightforward, but I swear this is a mere specialisation of the general definition of sheaves, only slightly simplified from the definition seen in textbooks.

Now, of course, sheaves support ifThenElse as we wanted, but the truly astounding thing is that the theory of sheaves tells us that the category of sheaves (and natural transformations forall i. p i -> q i) also has all the structure we need from the category of presheaves. In particular it’s Cartesian closed. Let’s demonstrate this next.

Closed Cartesianness

Products of sheaves are simply Haskell’s product applied fibrewise, same as with presheaves:

type (×) :: (Ty -> Type) -> (Ty -> Type) -> (Ty -> Type)
newtype (p × q) i = MkProd (p i, q i)

instance (Presheaf p, Presheaf q) => Presheaf (p × q) where
  pb f (MkProd (x, y)) = MkProd (pb f x, pb f y)

instance (Sheaf p, Sheaf q) => Sheaf (p × q) where
  glueIfThenElse b (MkProd (tp, tq)) (MkProd (fp, fq)) =
    MkProd (glueIfThenElse b tp fp, glueIfThenElse b tq fq)

Exponential objects are more complicated. If you’ve never seen exponentials of presheaves before, you can think of the type in terms of variance: because forall i. p i -> q i is contravariant in p, we can’t implement pb for natural transformation directly. So we freely adjoin the presheaf structure. Here again, the construction is the same for presheaves and sheaves.

type PFun :: (Ty -> Type) -> (Ty -> Type) -> (Ty -> Type)
newtype PFun p q i = MkPFun (forall k. Expr k i -> p k -> q k)

instance (Presheaf p, Presheaf q) => Presheaf (PFun p q) where
  pb f (MkPFun g) = MkPFun $ \k x -> g (compose k f) x

instance (Presheaf p, Sheaf q) => Sheaf (PFun p q) where
  -- This is not a typo, `p` only needs to be a presheaf.
  -- It's occasionally useful.
  glueIfThenElse b (MkPFun ft) (MkPFun ff) = MkPFun $
    \k x -> glueIfThenElse (k `compose` b) (ft k x) (ff k x)

I found that the twist in the definition of exponentials is the source of much of the difficulties in working with sheaves. For instance, this is why we need IfThenElse and glueIfThenElse rather than this more typical way of expressing that TBool is a coproduct of Unit and Unit:

cocone :: Expr TUnit i -> Expr TUnit i -> Expr TBool i
cocone t f = IfThenElse Id (Unit `compose` t) (Unit `compose` f)

glueCocone :: p TUnit -> p TUnit -> p TBool
glueCocone t f = glueIfThenElse Id (pb Unit t) (pb Unit f)

It turns out that IfThenElse is, in fact, strictly stronger than cocone in general. I started the project believing them to be equivalent, but they aren’t in general. They are equivalent in a Cartesian closed category (among other things) though, but Expr isn’t Cartesian closed. Textbooks also have a version of glueCocone, specifically that sheaves must verify that p TBool must be isomorphic to a pair p TUnit. Realising that this condition wasn’t sufficient to prove that PFun p q was a sheaf took me a while; and this is how, dear reader, one loses nights of sleep.

Yoneda embeddings as sheaves

Another thing, with our definition of sheaves, is that the Yoneda embeddings of objects Ty are sheaves. This won’t always be the case for the general notion of sheaves below, though.

instance Sheaf (Y i) where
  glueIfThenElse b (MkY t) (MkY f) = MkY $ IfThenElse b t f

Coproducts of sheaves

The category of sheaves also has coproducts, but they aren’t the same as that of presheaves. Coproducts of presheaves are defined fibrewise like products, but as we’ve been saying this is “too free”, in that it creates a coproduct for TUnit and TUnit which is distinct from TBool.

Fortunately, there’s a technical device which makes defining coproducts of sheaves easy: the free sheaf construction, also known as sheafification. It turns out that we can construct a free sheaf out of any presheaf, and the way you do that is to simply store all the uses of glueIfThenElse instead of running them (much like PFun stores all the uses of pb instead of running them):

data Sheafify p where
  Ret :: p i -> Sheafify p i
  ShIfThenElse :: Expr i TBool -> Sheafify p i -> Sheafify p i -> Sheafify p i

instance Presheaf p => Sheaf (Sheafify p) where
  glueIfThenElse = ShIfThenElse

instance Presheaf p => Presheaf (Sheafify p) where
  pb g (Ret x) = Ret (pf g x)
  pb g (ShIfThenElse b t f) = ShIfThenElse (pb g b) (pb g t) (pb g f)

The coproduct of two sheaves is simply the sheafification of their coproduct as presheaves.

newtype PSum p q i = MkPSum (Either (p i) (q i))

instance (Presheaf p, Presheaf q) => Presheaf (PSum p q) where
  pb f (PSum (Left x)) = PSum (Left (pb f x))
  pb f (PSum (Right y)) = PSum (Right (pb f y))

type ShSum p q = Sheafify (PSum p q)
-- Therefore:
-- instance (Sheaf p, Sheaf q) => Sheaf (ShSum p q))

You can also define recursive data types like lists (in categorical terms, polynomial endofunctors have initial algebras), you just have to make sure to wrap all the recursive calls with Sheafify. The easiest way is to inline Sheafify like so:

data ShList p i where
  ShNil :: ShList p i
  ShCons :: p i -> ShList p i -> ShList p i
  ListIfThenElse :: Expr i TBool -> ShList p i -> ShList p i -> ShList p i

Sheaves, generally

Now we have the general idea set up. Let’s tackle the general notion of sheaves. First we can get rid of Expr, and use an arbitrary category as a base.

-- The `Category` class from base.
type Category :: forall {k}. (k -> k -> Type) -> Constraint
class Category hom where
  id :: hom a a
  (.) :: hom b c -> hom a b -> hom a c

Presheaves readily generalise to arbitrary categories

type Presheaf :: forall {k}. (k -> k -> Type) -> (k -> Type) -> Constraint
class Presheaf hom p where
  pb :: hom a b -> p b -> p a

Topology, sites

We will need an extra piece of data in order to define sheaves, called a Grothendieck topology (I’ll just be saying “topology”). This will be the part that lets us choose which objects of the base category are to be colimits in the category of sheaves.

Before I show how we can represent topologies in Haskell, let us make a small detour and examine the textbook definition of sheaves (and reverting to mathematical notation for a moment). First a new notion: a sieve on an object $a$ is a set of arrows with codomain $a$ closed by precomposition. That is a set $S$, such that for any $(x \stackrel{f}{\longrightarrow} a)\in S$ and any arrow $(y \stackrel{g}{\longrightarrow} x)$, we also have $(y \stackrel{g}{\longrightarrow} x \stackrel{f}{\longrightarrow} a)\in S$. A topology is a set of such sieves (subject to some axioms). Sieves in a topology are called covering sieves.

Let $P$ be a presheaf. A matching family in $P$, for a covering sieve $S$ on $a$, is a function $m$ mapping each $(x \stackrel{f}{\longrightarrow} a)\in S$ to $m_f ∈ P(x)$, such that $m_{f . g} = \mathsf{pb}(g) (m_f)$. Then, $P$ is a sheaf if for every such matching family $m$, there is a unique $\mathsf{glue}(m) \in P(a)$ such that $m_f = \mathsf{pb}(f) (\mathsf{glue}(m))$ for all $f ∈ S$.

Now, this is an extraordinarily compact definition. It achieves a lot in just a handful of axioms. But it’s also a very wasteful definition. The definition of sieves requires that all the $(y \stackrel{g}{\longrightarrow} x \stackrel{f}{\longrightarrow} a)\in S$ are arguments of $m$, but at the same time that $m_{f . g}$ is determined by $m_f$.

This is very unsatisfactory from a functional programming perspective, as we like to make illegal things unrepresentable, but the mathematical definition gives us infinitely many ways to represent illegal states. Besides, having many irrelevant values to take into account adds unwanted noise to our programs.

Even if you are fine with those issues, there’s a bigger problem. The implementation of gluing for functions (much for the same reason as functions needing the full IfThenElse rather than merely cocone) necessarily involves a sieve, called the pullback sieve $f^*S$ where ($b \stackrel{f}{\longrightarrow} a)$ is an arrow and $S$ is a sieve on $a$; $f^*S$ is, then, a sieve on $b$. And this is too much dependent typing for even Haskell. I’ve tried to make it work but couldn’t.

Which leads us to our first simplification: we don’t need covering sieves, we can consider arbitrary covering families of arrows (the corresponding covering sieve is the sieve generated by those arrows, but it’ll only exist in our head). Our second simplification is that we don’t even need covering families to be families of arrows: arbitrary types will do. This will remove most of the obstacles, and the pullback sieve won’t show up at all.

In ordinary mathematics, a topology is a set of sets. The natural way to represent this in types is as a type indexed by another type, which yields our definition of topology, or rather of a site: a category equipped with a topology.

type Site :: forall {k}. (k -> k -> Type) -> Constraint
class Category hom => Site hom where
  data Cover hom :: k -> Type
  data Gen hom :: Cover hom a -> k -> Type

Where Cover hom a is the type of covering families of a (typically, Cover hom a is simply an enum of names), and Gen hom c is the type of elements of the covering family c (which we think of as generating a covering sieve, hence the name).

Sheaves on a site

Now sheaves are given by the following type class:

class (Site hom, Presheaf hom p) => Sheaf hom p where
  glue :: forall {a} (c :: Cover hom a) b. hom b a -> (forall x. Gen hom c x -> p (x × b)) -> p b

(I’ve cheated a little and assumed that the underlying category is Cartesian; we can get rid of this hypothesis by replacing p (k × b) with the equivalent, but considerably more heavyweight, PFun (Y x) p b)

This definition includes one trick that I haven’t described yet: with a cover c :: Cover hom a instead of gluing only at type p a, we need to be able to glue at type p b for any arrow f :: hom b a. This is how we avoid having to talk about a pullback sieve. And this also seems to be why generators don’t need to be actual arrows.

To elucidate this definition, let’s see how to instantiate it to Expr¹

instance Site Expr where
  data instance Cover Expr i where
    BoolCover :: Cover Expr TBool

  data instance Gen Expr c k where
    TrueCovers :: Gen BoolCover TUnit
    FalseCovers :: Gen BoolCover TUnit

glueIfThenElse :: (Sheaf Expr p) => Expr i TBool -> p i -> p i -> p i
glueIfThenElse b t f = glue @_ @BoolCover b $ \g -> case g of
  TrueCovers -> pb snd t
  FalseCovers -> pb snd f

To show a bigger example, one that makes use of the x parameter in p (x × b) (so far we’ve simply ignored x, since it’s always been equal to Bool), let’s extend the arithmetic expressions with a sum type:

data SumTy = … | TSum a b

data SumExpr i j where
  … -- Like Expr
  Left :: SumExpr i j -> SumExpr i (TSum j k)
  Right :: SumExpr i j -> SumExpr i (TSum k j)
  Case :: SumExpr i (TSum k j) -> SumExpr (k × i) l -> SumExpr (j × i) l -> SumExpr i l

In order to be able to pattern match on sums in the category of sheaves, we will have to add a cover for TSum. As the type of Case suggests, we will use the x parameter to pass the value contained in Left or Right.

instance Site SumExpr where
  data instance Cover SumExpr i where
    BoolCover :: Cover SumExpr TBool
    SumCover :: forall a b -> Sum.Cover (a `TSum` b)

  data instance Gen SumExpr c k where
    TrueCovers :: Gen BoolCover TUnit
    FalseCovers :: Gen BoolCover TUnit

    LeftCovers :: Gen (SumCover a b) a
    RightCovers :: Gen (SumCover a b) b

This is equivalent to saying that sheaves for SumExpr have two gluing functions, glueIfThenElse and glueCase, such that in glueCase the Left alternative is passed an a and the Right alternative is passed a b, like we expect of a case expression.

Now, all instances from the previous section can be written in this abstract style. Except the instance for the Yoneda embedding. In particular, if you add a covering family for an object which isn’t a colimit in the base category, then the Yoneda embedding won’t yield sheaves. If you want to look this up, topologies where the Yoneda embedding only yields sheaves are called subcanonical.

Further reading and final thoughts

If you want to see the actual instances for the abstract definition of sheaves, you’ll find them in this file. In there the site is actually concrete, but the instances are written as if it were abstract.

For those who want to read even more, I wrote some other thoughts on the project on Bluesky which you may enjoy. If you are type-theory inclined, you will probably enjoy Pierre-Marie Pédrot’s Pursuing Shtuck, it helped me a lot with figuring these things out (it left quite direct a mark on the project – for instance I lifted the definition of the sheafification functor directly from there).

When I started trying to implement sheaves I didn’t know whether it would work. Sometimes it pays to be stubborn enough. But also, implementing a project like this lets you confront the finer details. Here’s one: in my definition of Expr there is no fixed point. Recursive functions like fact and fib simply compile to infinite Expr trees (which is fine as long as you keep Expr lazy enough). And the truth is: I don’t know how to add fixed points in a way that could be lifted to sheaves (via a sheaf condition or otherwise). It might not be possible at all (if you know something about that, get in touch!). Anyway, now, at least, I know what I don’t know.