Modal HoTT on the Web
On Dependent Sums and Products
(this is research in progress)
Below I start by giving some background on how I came to discover the new foundation mathematics HoTT by talking to Odersky creator of Scala and how recently I discovered Modal HoTT, which should be useful for my work in Web Security. Reading about Modal HoTT lead me to grapple with how Dependent Types map to Categories. I hope the text below will help make this clear to myself and to others too.
Background
Close to 5 years ago I went to Scala Exchange to give a talk on the Scala library banana-rdf and the purpose for which it could be used for a project that is now known as Solid a platform to redecentralize web applications. (Note: the company behind Scala eXchange went bust this week beginning Nov 2019 so the video is no longer available)
At some point I found myself sitting at a table with Scala creator Martin Odersky. I told him how Scala had helped me rediscover mathematics via the scalaz libraries (the predecessor to Cats). I had found Free Monads to be very helpful in writing a Solid web server, and this had lead me to start reading a few book on Category Theory. During the conversation Odersky mentioned that there was a new foundational mathematics called Homotopy Type Theory (HoTT). That really struck me: those don’t appear every day, more like once a century. So I was very intrigued and downloaded the open source HoTT book on coming home. Here is an article by Wired on how HoTT came to be:
The first few chapters of the HoTT book are very accessible to any programmer and very much worth reading. Central to HoTT are dependent types. As it happens these are also central to the next version of Scala whose Dotty compiler is based on DOT, the calculus of Dependent Object Types (see The Essence of Dependent Object Types).
As I worked my way through the HoTT book, I was wondering as to how much it had to say on modal logic, as I had a feeling that those would be very useful to working in security (widely confirmed by my later investigation). Indeed there is a chapter 7.7 on modalities but it is very short. So I let that go, and on reading Modal Logics Are Coalgebraic a few years later, explored the very interesting field of coalgebras instead.
Just a month ago on my Twitter feed I found that a new book on Modal Homotopy Type Theory was about to come out, by David Corfield, who is also one of the originators of the ncatlab Category Theory wiki. An early version of Chapter 4 of the book had already been published in 2018.
Getting to HoTT via modal HoTT may seem like starting from the deep end. On the other hand, when studying analytic philosophy I saw how much modal logic transformed the field from the 1960ies onward, revolutionizing most areas from logic to philosophy of language, leading to very powerful analysis of concepts such as counterfactuals, knowledge, belief, causality, .... These are essential concepts that we use in our everyday thinking. A maths without modal logic felt like it would be missing the most important tool I needed for an analysis of the web. Luckily this is no longer the case.
Dependent Types practically
Practically, Dependent Types are not that difficult to understand. With programming language such as Idris that focus on them, one can learn by seeing how they are used to write programs.
In chapter 1 of HoTT two dependent types are described: Dependent Functions and Dependent Pairs.
Dependent Functions
In normal functional programming a function has a domain and a range, written f: A → B . Such a function takes any object of type A and returns an object of type B. For example
len: String → ℕ
takes a string of characters and returns its length, 0 for the empty string “”, 1 for single characters “a”, 5 for “hello”, etc… All the returned values are numbers.
A dependent function on the other hand can return different types of objects depending on the input value. For example, when parsing an HTTP response from a web server the type of the resulting object will depend on the media type discovered in the parsed byte-string. If it is “text/plain” then the returned object could be a utf-8 string. On the other hand if the type is “image/jpeg” then the returned type could be an image, “audio/*” could return an audio object, “video/*” a moving image, “data/*” a data structure, … These are all objects of very different types that get processes and manipulated in very different ways.
The HoTT book in §1.4 introduces these as Dependent Function Types. They require the notion of a stack of Universes of Types 𝒰 (§1.3) and families of types, which are functions at the type level from types to a Universe of types 𝒰. So we can define
Parse: Bytes → 𝒰
as a family of types, which for every string of Bytes returns a type in the Universe 𝒰. One can then write a dependent parse function as
parse: ∏(x: Bytes) Parse(x)
which if it were to parse the bytes returned by Tim Berners-Lee’s WebID Profile, described below, would return an RDF Graph.
Dependent Pairs
Pairs of objects are very common. For example pixel positions on a screen will be identified by pairs of integers (x,y): ℕ×ℕ ≡ Pos. A pixel may be a color and a position, as these are completely independent of each other, so we can have a blue pixel at position (20,678)
(blue,(20,678)): Color×Pos.
A dependent pair is similar, except that the type of the second element depends on the value of the first. A very widely used simple version of this is the Either[A,B] type which is either an A or a B. How does A depend on B? you may ask. Well (usually) they don’t. But the way coproducts A+B — also known as disjoint sums — are implemented is that object from each type are mapped to a pair consisting of a marker for their position (left or right) and the value. The marker might as well be an element from 2 the type with two objects. Below are two instances of the String+Dom coproduct type, the first an error and the second a successful parse where dom is a Document Object Model.
(0,”parsing error line 10"), (1,dom): String+Dom
An example David Corfield uses, starts with two types: Football Players (FPlayer) and Football Teams (FTeam). The product FTeam×FPlayer gives the space of all ways of pairing players to teams with many nonsensical combinations. Instead given a Player type-level-function which assigns to each Team the type of all players for that team.
Player: FTeam → 𝒰
we can construct the dependent pair type
(Chelsea,Hazard): ∑(t: FTeam)Player(t)
which is the set of pairs of a team and a player in that team. According to Wikipedia Eden Hazard is a player in the Chelsea Football team, which is my warrant for the above assertion.
On the World Wide Web it looks like we have a dependent product when modelling fetching a URL. Take for example Tim Berners-Lee’s WebID (a URL that denotes him ), call it timbl, and the graph that is its sense which we obtain by applying the stream of bytes returned by the W3C server to our parse function defined above. Name the graph timblGrph.
Then we have the dependent pair
(timbl, timblGrph): ∑(x: URL) GET(x)
which we call a Named Pointed Graph, naming the node highlighted in yellow inside the Named Graph, which is the pair of a name and a graph fetched at that location. We can get the name of the graph simply by splitting the WebID at the URL #fragment identifier. (A faithful modelling of HTTP would be more complicated than this, as the result of a GET is likely to be a more complex structure such as a Error+Graph, if one wants to take into account that not all URLs are dereferenceable).
Here we can see how modal logic starts playing an important role. As with the football teams whose members depend on the state of the world (they vary over time) and indeed, if the world described is actual or fictional, so it is with which representations are returned by a GET request on the Web, and even more so for the World Wide Web and so the Semantic Web. For what is published at a server like the W3C depends on the fact that the World Wide Web consortium bought the w3.org domain. The links on those pages point to other servers around the world, that were selected because of their content. The names of the relations used depend on various arbitrary decisions made at various points in time in standards bodies, … The same is true of this page, which contains links to other pages and embedded content.
Thus, we may want to add the state of the web to our model, giving us
(@,(timbl, timblGrph)): ∑(w: WWWState)∑(x: URL) GET(w, x)
with @ denoting the actual state of the world. Btw, this also indicates why coalgebras, the mathematics of states and observations, comes into play as we are dealing with an evolving system. Hopefully, we will be able to work out more clearly what this means in Modal HoTT.
Dependent Types in Category Theory
Reading Chapter 4 of David Corfield’s Modal Homotopy Type Theory preprint, I realised on re-reading it carefully, that I was getting a bit confused. I thought I’d make sure I understood the basics. This lead me to look up the Dependent Sum page on nLab, as those play a key role in the explanation of modal types.
It takes some skill to learn how to read the nLab wiki. The information is very condensed, requiring one to follow links to other pages in hope of an clarification, but those often explain the concept in even more abstract terms with even more pages to open. When I first started 4 or 5 years ago, I often ended more confused.
The biggest transformation came after I listened to a whole series of online videos by Bartosz Milewski, where he shows by regularly drawing out the diagrams how these are to be understood and ties CT concepts to practical programming problems, as well as giving some big picture views from time to time as to how this ties in with say HoTT. He has now published a free online book Category Theory for Programmers, one of which has both Haskell and Scala examples. For Object Oriented Programmers I recommend to also read some of the articles from the 1990ies by Bart Jacobs (some pointers here), describing that OO also can have a Category Theoretic interpretation in terms of coalgebras and how these are strongly connected to Modal Logic. Having Category Theory explained in terms of a field one understands very well, makes a huge difference to how easy it is to form intuitions. For those with more experience with Databases, I recommend reading Spivak’s Category Theory for the Sciences.
After not finding the right material on Google Scholar I decided to start my research by posting a question on Twitter, as a way to remind myself what my task was.
The Nlab page makes clear that the most basic concept (aside from a Category) is that of a slice category. These play a key role in the explanations of dependent types. That helped me refocus my interest in them.
As a quick reminder: a Category is composed of objects and arrows between objects, written f: A → B, such that every object has an identity arrow ida: A → A, arrows compose when they have the same endpoints f: A → B, and g: B → C compose to a new arrow h: A → C, such that f;g = h and the composition with the identity arrow does nothing ie. f;idB = idA;f = f . Finally the arrows are associative so that f;(g;h) = (f;g);h.
In the Category of Sets, a.k.a Set, the objects are sets and the arrows functions between them. Sets are the simplest form of Topos, a concept that brings together logic and geometry. Any Topos Category allows one to take an object from it and form a slice category. ( Fong and Spivak’s recent “7 Sketches in Compositionality: An Invitiation to Applied Category Theory” with online videos has chapter 7 dedicated to Topoï).
Slice Categories
A slice category 𝒞/c of a category 𝒞 over an object c of 𝒞, has as objects all morphisms f ∈ 𝒞 such that the codomain (a.k.a range) of f is c, and as morphisms g: X → X’, from objects f: X → c to f’: X’ → c such that g;f’ = f.
Until recently I found it difficult to see what was interesting about them. Their relation to HoTT piqued my interest, and the first chapter of “7 Sketches in Compositionality” helped give me some intuitions, as the authors shows how an function f: A → c can be also seen as a way to partition A (especially when f is onto, ie covers the whole of c). So given one object (type) A → c in 𝒞/c all functions from that to another type B → c have to keep the ‘elements of A’ mapped to elements in B living in the same partition.
The simplest Slice category is 𝒞/1 where 1 is the final object of 𝒞, namely an object that has only one arrow coming in from every object in that category. In Set, 1 is any singleton set. (Any Topos has finite limits and so I believe a final object). Given that all objects of 𝒞 have only one morphism to 1, any arrow to 1 partitions an object into one single partition, namely itself. As a result there is no difference between 𝒞/1 and 𝒞.
The next simplest object is 2, an object with 2 elements in Set, where it is also known as the subobject classifier; because one can define any subset of a set A by a function ∈ : A → 2, namely the one that sends elements of the subset to ⊤ and the others to ⊥.
Above is a very small extract of the objects of Set/2: the objects are the rounded rectangles in black related by a black arrow to the central 2, and the morphisms between those objects are shown in red. It looks like we have Set duplicated twice: everything connected to the object 1→⊤ looks similar to Set, and so is everything connected to 1 → ⊥. We have as initial object 0: ∅ → 2 and as final object id2: 2 → 2 . We can see how every surjective function onto id2, splits the sets into 2 parts. That should give some intuitions as to what a slice category looks like, hopefully enough to follow this short lecture.
Pullbacks of two functions f: A → X and g: E→ X is the subset Æ of the pairs A×E where for each æ: Æ ⊆ A×E, f(π1(æ)) = g(π2(æ)) . When X = 1, then Æ = A×E, since any combination of A and E maps to the only element * of 1.
So pullbacks give us subsets of pairs, and the lecture above tells us how products in slice categories are pullbacks. which means that we do seem to be somewhere close to dependent pairs. So we are on the right track.
Dependent Sums
Now the Dependent Sum NLab page tells us that to understand Dependent Sums we have to look for the left adjoint to the base change functor between two slice categories. Phew! That’s a steep climb.
Adjoint Functors are one of the key concepts of Category Theory and introduced in 1958 by Daniel Kan a Dutch Mathematician working in Homotopy Theory (!). He is also behind what is known as a Kan Extension, which Saunders Mac Lane described in “Categories for the Working Mathematician” in a section titled “All concepts are Kan Extensions”.
Before that one needs to know what functors are. Simply put: these are arrows between categories in the category of categories, where categories are objects. A functor F between category ̅𝒞 and category 𝒟, written F: 𝒞 ⇒ 𝒟 maps all objects of 𝒞 to objects of 𝒟 and all morphisms of in 𝒞 to morphisms 𝒟 so that the map respects source, target, composition and identity (see nlab page).
Adjoint Functors are functors that go between two categories in the opposite direction, so that their combination gives something that just somewhat weaker than equality to be interesting. Here is an article from Wired that goes into the importance of this weaker than equality phenomenon.
Adjoint functors are everywhere. They give rise to monads and comonads, that David Corfield shows in his Modal HoTT paper to be what is needed to interpret modal logical concepts such as possibility and necessity. We’ll see a few examples below.
Anyway luckily I got a bit of help to interpret the nLab page on dependent sums.
To help me visualize this I drew the adjunction out for the simplest base after 1, namely 2. So in the following diagram I just set David Corfield’s A to be the type 2 of two ojects {1, 2} . On the right we have the 𝒞/1 category and on the left the 𝒞/2 slice category with the f* functor going left, and the ∑f functor going right. (left adjoints start on the left and go right). The adjunction states that there is a bijection (1 to 1 relation) between the set of functions between D and 2×B on the left, and between ∑f and B on the right (plus a naturality condition). The arrows in gray on the right are to illustrate some reasoning later on.
First it will help to try to make intuitive sense of it. It is clear that the base change functor f* that maps objects B of 𝒞 to the function π1: 2×B → 2 (which is an object in 𝒞/2) will also correctly map any function f: C → B in 𝒞 to a morphism 2×f: 2×C → 2×B in 𝒞/2 (leaving out the projections to 2). This is clear because in those products the right hand side is completly independent of the left, which is mapped via a projection to 2. Note: this will map 1 in 𝒞 to π1: 2×1 → 2≅ id2: 2→ 2 in 𝒞/2 which is also the final object there.
If we have an object g: D → 2 in 𝒞/2 and given a map h: D → B in 𝒞 then there will be only one map <g,h>: D → 2×B which combines g and h. (see nlab product page). I have drawn <g,h> above in both categories, though the full product diagram is only shown in the left category. Still we see that the diagram in 𝒞/2 containing two objects, is just one triangle of the product diagram on the right.
In 𝒞 we find the object ∑(x:2) D(x) that is generated from the object g in 𝒞/2 . The ∑f functor just maps the objects of 𝒞/2 as is to 𝒞, so nlab tells us. How can it do that? Are not objects in 𝒞/2 functions, and objects in 𝒞 Sets? Well, if we think of functions as special types of relations, as they are traditionally thought of in Set theory, then we can think of g: D → 2 just as a subset of pairs D×2 with each element of D mapped to only one element of A. We can then just flip this set of pairs around and get a subset of pairs 2×D that have the same restriction. It is a bit different as not every element of 2 will be related to D, and some elements of 2 may be related to more than one D. So that give us something that looks like what we are looking for. We also can prove in Agda that ∑(x: 2) D(x) is equivalent to the coproduct D(0) + D(1). Here D(0) is the subset of D which g takes to 0 and D(1) is the subset of D taken to 1 by g. So we can also draw those two functions as inr and inl in the diagram for the category 𝒞 .
Here is the same diagram now generalized to any type A instead of just 2.
As mentioned above an adjunction is a bijection of HomSets, which in the case above states that there must be as many morphisms between D and A×B as between ∑(x:A)D(x) and B. We stated that for any given g: D → A and h: D → B, we have only one morphism <g,h>: D → A×B in 𝒞 as well as 𝒞/A. π2 is fixed, and so we see that selecting any g and h, identifies one function on both sides: in 𝒞/A we have <g,h> and in 𝒞 we have π2;h: ( ∑(x:A)D(x)) → B . (todo: one has to show that the family of bijections is also natural in B and D)
I have also shown in 𝒞 that ∑(x:A)D(x) is the pullback of idA and g, that is for any ad: ∑(x:A)D(x), we have π1(ad) = g(π2(ad)).
Looking at this I am struck by a difference of emphasis from the presentation in HoTT. Here the dependent types of D are it seems subsets of D, and indeed we will see shortly that the subsets are the stalks of D over A. In HoTT this is the function D: A → 𝒰, where for every a: A, D selects a type in the universe 𝒰. It does match since subset/subtypes of D also exist in the universe.
So now that I am confident in the structure of the adjoints, we see how it fits a real life example. David Corfield puts it in terms of football teams.
And it is very easy to follow that reasoning now by looking at the above diagram.
Dependent Products
David then suggests looking at the right adjoint, which gives us the dependent product. The NLab Dependent Product page starts talking about fibres, bundles, and sections of a bundle, but does not add a picture to make the intuitions clear. So I remembered coming across Robert Goldblatt’s “Topoï: The Categorical Analysis of Logic” initially published in 1979, (republished 1984 and 2006), that goes over this field carefully, explaining every concept as required.
The picture to the left is a simplified view of a sheaf. It consists of a bundle of sets Ak, Ai, Aj,… whose union in Set is A, over a base space I={k,i,j,…}. This corresponds to a function p: A → I where all elements a of A that have the same value p(a)=i are grouped together in the stalk (or fiber) over i. The members of Ai are called the germs at i. The metaphor is that of a wheat stalk shown in the picture below (thanks to Max Pixel). One such function creates a bundle of sets.
And so we can also consider a slice category as a bundle category. Functions between bundles of the same base space, take germs over i from one object of the category to germs over the same i in another object of the category. This allows us to make assertions over a “bunch” of sets at the same time.
This is also clearly layed out with nice exercises in §7.3.3 of Seven Sketches of Compositionality.
This just leaves us to explain what a section of a bundle is. As I don’t know much about football, I’ll use an example I understand as I have 3 kids that go to kindergarten. All the kids in the kindergarten are divided into groups G, named after cute animals like penguin, sheep, butterfly, etc… as depicted below. So we have a function in: Kids → G . With this we can form a slice category Set/G, whose final object is IdG. Any function from a final object 1 in Set a to another object (ie. a Set) identifies one element of that set known as a global element. Here to a function from the final G to any other object slice: G → Kids selects one element from each germ in the bundle Kids (in yellow below) as show by the purple arrows. Any such function can be seen to be a dependent function, if one considers the range to be the germs, and all of them together form the dependent product type. Following from the first section of the Dependent Product page, the cartesian product of each of the bundles is the set S of global sections of the bundle. It contains for example the triple<A, Linus, Anaïs>. Consider S×G shown on the right as an element of the slice category, that is as the obvious projection π4: S×G → G, then the evaluation function ev: S×G → Kids must work like this:
<A, Linus, Anaïs,🦋> ↦ Anaïs
<A, Linus, Anaïs,🐑> ↦ Linus
<A, Linus, Anaïs,🐧> ↦ A
This S is such that given any T and morphism T×A → G there is a unique map T → S that makes everything commute. This it seems according nlab is what makes the adjunction below.
The rest of the Dependent Product page on nlab is very difficult to follow as it introduces notation such as [X,P] 𝚪x and {id} that is not defined on the page.
It should now be easier to follow the rest of David Corfields football example.
(Note that for some reason nlab, has on which the diagram is based has B×A reversed from David’s description). Remember we have A = teams, D a collection of team players, and now B people interested in the sport.
Yes, the functor f* sends B to B×A → A and so in the stalk above each a: A, we have for each b: B the pair (b,a).
Modal HoTT
The above is enough material for one blog post, but also enough I hope to follow clearly David Corfield’s Chapter 4 on Modal HoTT.
At the beginning of his paper he speaks about how a function owner: Dog → Person induces a functor owner*: 𝓟(Person) ⇒ 𝓟(Dog), between the Properties categories of Person and Dog, i.e. the Powersets of Person and Dog ordered by subset inclusion, where these adjunctions also hold.Later he moves on to slice categories of a Topos, which is where the above reasoning comes in.
An interesting point made is that in a slice topos H/C (and Set is a topos), then C is the context. One such context is the context of Worlds W, where the fibers of H/W represent the properties of what is true at W…. But there is a lot more there than I can write in this post, and there is no need to duplicate it. Also I look forward to reading more of the documents on the NLab Modal HoTT page.
