Discussing "Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom"

(Link)

Authors: Cyril Cohen (INRIA Sophia Antipolis - Méditerranée), Thierry Coquand (University of Gothenburg), Simon Huber (University of Gothenburg), and Anders Mörtberg (Institute for Advanced Study)

Reference: Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg, Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015), ed. Tarmo Uustalu, Leibniz International Proceedings in Informatics (LIPIcs), vol. 69 (2018).

Why this paper? Cited by Formalizing CCS and π-Calculus in Guarded Cubical Agda and Normalization and coherence for ∞-type theories

I’ve blogged a few times on homotopy type theory, ranging from the seminal book to various follow-ups (One Two Three). This is one of the most important follow-ups because of what it does to the univalence axiom, the cornerstone of homotopy type theory that asserts that equivalences between types correspond to identities between them. Cubical type theory is an instance of homotopy type theory for which the univalence axiom is not an axiom at all, but rather a provable theorem (inhabited type). The significance of this may not be immediately obvious to newcomers to type theory – who cares if a statement is an axiom or a consequence of some other rules? In fact with the type theories that lend themselves to applications such as interactive theorem proving we do not typically proceed by asserting axioms – unless we need to – but rather by defining rules for introducing and eliminating our basic type formers. Arranging things in this way allow us to have good computational properties, for example a constructive argument involving a natural number really will produce an appropriate natural number when run. This gives proofs in the type theory computational content, whereas the bald assertion of an axiom would provide a ‘roadblock’ in the execution of a proof.

This development proceeds by developing a type theory which has denotational semantics in the category of cubical sets. In this blog post I won’t sweat the details of these semantics – many of my comments last week about semantics in simplicial sets still apply  – although it is important to understand that working via the semantics motivates every part of this paper. However, I wish to concentrate on the details of the type theory itself as syntax.

It is fair to say that cubical type theory is a heavy duty extension to standard type theory. Some of the earlier parts of the paper are quite beautiful, however. The notion of identity as path is captured by thinking of them as (roughly) a function from a slightly abstracted version of the real interval [0,1] to a type; if we wish to express that t is equal u then we need that function to map 0 to t and 1 to u, and we’re done. This gives a startlingly simple proof of function extensionality (functions are equal if they agree on all inputs), which is a tricky property, and indeed sometimes not even true, in many type theories. Things get more involved, but still rather elegant, if we want dependence on multiple different arbitrary elements of the interval, usually called dimensions. This is where the cubes of cubical type theory come in, as zero dimensions give rise to a point in a space (which is to say, just a usual inhabitant of a type), and one dimension to a path in a space, but we can have squares, cubes, 4-dimensional hypercubes and so on as well.

The next feature is to define faces, which can be thought of as corresponding to faces of cubes (of various dimension), or more prosaically as restrictions on the values that our otherwise arbitrary interval elements can take. For example, we might require that both i and j are equal to one of 0 or 1, describing the outline of a square but leaving its centre unfilled. Terms and types defined with faces in their context are then only partial, e.g. only existing where the free dimensions i and j have appropriate values. Systems are terms of arbitrary type that explicitly define different constructions for different faces. Faces are also used to introduce the notion of extensibility;  a partial term t with respect to face φ is extensible if there is a term u that is not restricted to φ, for which if φ is added to its context, it is indeed equal to t. A new composition operator then comes into play that ensures that extensibility is preserved along paths. This may seem heavy, but is necessary to prove the rather mundane fact that identity is transitive. The equality judgements (intuitively, reduction rules) associated with the composition operator are fairly complex, depending on the type the composition is applied at and so needing explicit definition corresponding to each type former.

The final layer of novelty involves a new type former called glueing which connects types with partial types, and ensures that extensibility is invariant across equivalence. This is the final necessary ingredient for univalence (which is a statement about equivalences, after all) to be proved.

Discussing "Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type"

(Link)

Authors: Thorsten Altenkirch (University of Nottingham), Nils Anders Danielsson (University of Gothenburg), Nicolai Kraus (University of Nottingham)

Reference: Altenkirch, T., Danielsson, N.A., Kraus, N. (2017). Partiality, Revisited. In: Esparza, J., Murawski, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2017. Lecture Notes in Computer Science(), vol 10203. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-54458-7_31

Why this paper? Cited by A metalanguage for cost-aware denotational semantics, and Streams of Approximations, Equivalence of Recursive Effectful Programs, and Executable Denotational Semantics with Interaction Trees

A couple of months ago I wrote about Moggi’s seminal work on monads, which can be used both to write, and to reason about, code with side effects. A side effect is any operation of a program which is not most naturally thought of as an output, and this paper concentrates on one such notion – the program potentially failing to terminate and produce an output at all. The option to fail to terminate is a crucial feature of most real programming languages, because without it, a language fails Turing completeness, and so is not as expressive as it might be.

Following Capretta, possible non-termination can be modelled by the delay monad. This is a construction which allows outputs to be ‘delayed’ any number of times, and perhaps indefinitely. Elements of the monad therefore carry a trace of how many times they were delayed - very roughly speaking, how many steps of some computation was required to produce them, a concept we have seen before. However for some purposes in reasoning about programs, one wishes to ignore the number of steps taken, and merely talk about the output (if there was one). We do this by quotienting the monad to ignore any finite number of delays. This makes the delay monad a monad in the category of setoids – sets equipped with an equivalence relation.

Unfortunately working formally with setoids may consign one to what is colourfully called ‘setoid hell’, where one has the tedium of proving that every construction, no matter how apparently unconnected to the notions of termination and delay, must respect the equivalence relation. An alternative is working in a type theory with quotient types, but this turns out not to work as well as expected, either failing to produce a monad (and hence, a well behaved model of the side effect) at all, or requiring a powerful extra mathematical property called countable choice to make things work.

This paper is influential because it shows that a proper delay monad can be constructed without invoking any new mathematical axioms if we allow ourselves to construct quotient inductive-inductive types (QIITs). Quotient inductive types are a limited form of the higher inductive types of homotopy type theory; the ‘inductive-inductive’ part of the term means that a type and a construction on the type are defined inductively at the same time. Given this technology, the delay monad, quotiented by ignoring finite numbers of delays, is finally shown to behave as it should.