Partiality (Type Theory)

Definition

In type theory, partial functions can be represented by several different monadic constructions. The most useful names are the maybe monad, the semidecidable lifting monad or non-termination monad, the delay monad, and the full partial-map-classifier monad.

The maybe monad, the semidecidable lifting monad, and the full partial-map-classifier monad are instances of the lifting pattern. The delay monad is different: it records delay steps coinductively rather than classifying partiality by propositions.

Constructions

Construction	Name	Other common names
$A+1$	maybe monad or option monad	decidable partiality monad
Partiality classified by semidecidable propositions	semidecidable lifting monad	non-termination monad, Sierpinski lifting, Rosolini lifting
$\nu X.A+X$	delay monad	Capretta’s delay monad, coinductive partiality monad
${\Sigma }_{P:\mathsf{Prop}}(P\to A)$	full partial-map-classifier monad	propositional lifting monad, full lifting monad

The semidecidable lifting monad is usually called the partiality monad or non-termination monad, not Capriotti’s monad.

Related Concepts

Delay Monad
Lifting Monad
Maybe Monad
Type Theory