Lifting Monad

Definition

In type theory, the lifting monad is a way of representing partiality. A lifting monad is a construction of the form

$$L_{\mathcal{D}}(A):={\Sigma }_{P:\mathcal{D}}(P\to A),$$

where $\mathcal{D}$ is a chosen set of propositions.

An element of $L_{\mathcal{D}}(A)$ consists of a proposition $P$ expressing when the partial element is defined, together with a function $P\to A$ producing a value under that assumption. In this way, the lifting construction represents partial elements of $A$ whose domains of definition lie in $\mathcal{D}$.

When $\mathcal{D}$ is suitably closed, this construction carries a monad structure. Different choices of $\mathcal{D}$ give different notions of partiality.

$$\begin{array}{rl}& (P,x)>>=f=(P\wedge Q),\lambda (p,q).f_0(x(p))(q)\\ & \mathrm{return}(x)=(\top ,\lambda \_\to x)\end{array}$$

where $(Q,f_0)=f(x(p))$.

Examples

• If $\mathcal{D}$ is the class of decidable propositions, then $L_{\mathcal{D}}(A)$ is equivalent to $A+1$, the maybe monad or option monad.
• If $\mathcal{D}$ is the class of semidecidable propositions, then one obtains the semidecidable lifting monad, also called the non-termination monad or Sierpinski lifting.
• If $\mathcal{D}$ is the class of all propositions, then one obtains the full partial-map-classifier monad.

Related Concepts

Maybe Monad
Partial Function
Partiality (Type Theory)
Unbounded Minimization