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.