Quotiented delay monad as the initial ω-join classifying monad

Niccolò Veltri

Institute of Cybernetics at TUT

Monday, 29 August 2016, 14:00 (note the unusual weekday)
Cybernetica Bldg (Akadeemia tee 21), room B101

Abstract: The delay monad was introduced by Capretta as a means to deal with partial functions (possibly non-terminating programs) in type theory. It is often desirable to consider two delayed computations equal, if they terminate with equal values, whenever one of them terminates. The equivalence relation underlying this identification is called weak bisimilarity. In previous work, we have shown that the delay datatype quotiented by weak bisimilarity is also a monad, if we extend type theory with extra principles such as countable choice and propositional extensionality. Moreover, we proved that the quotiented delay datatype delivers free ω-complete pointed partial orders (ωCPPO for short). As a consequence, homsets in the Kleisli category of the quotiented delay monad are endowed with a ωCPPO structure.

In this talk we introduce the notion of ω-join classifying monad. A classifying monad is a monad whose Kleisli category is a restriction category (that is, an axiomatic formulation of categories of partial functions introduced by Cockett and Lack). In every restriction category, it is possible to define an order on homsets, the so-called restriction order, and this order specifies a Poset-enrichment on the category. A ω-join classifying monad is a classifying monad whose restriction order specifies a ωCPPO-enrichment. We show, using the results from previous work, that the quotiented delay monad is a ω-join classifying monad. Interestingly, it is also the initial such monad.

Tarmo Uustalu
Last update 24 August 2016