Partiality Monad

Definition

The partiality monad on a type $A$ models computations that may either return a value of type $A$ or diverge. In Type Theory it is used to represent partial functions inside a total language.

In intensional type theory, a direct presentation is as a quotient inductive-inductive type: one simultaneously defines

• a type $A_{\perp }$ of partial elements of $A$
• a relation $\le :A_{\perp }\to A_{\perp }\to \mathrm{Set}$
• an equality relation on $A_{\perp }$

with the intended meaning that $(A_{\perp },\le )$ is an $\omega$-complete partial order with a least element.

QIIT presentation

Let $c$ range over $\omega$-chains in $A_{\perp }$, where an $\omega$-chain packages both a sequence $\mathbb{N}\to A_{\perp }$ and a proof that it is increasing.

The constructors for $A_{\perp }$ can be written as inference rules:

\dfrac{x : A}{\eta(x) : A_\bot} \qquad \dfrac{}{\bot : A_\bot} \qquad \dfrac{c : \omega\text{-}\mathrm{Chain}(A_\bot)}{\bigsqcup c : A_\bot} \end{aligned}$$ Thus $A_\bot$ contains ordinary terminating values, a divergent element $\bot$, and suprema of increasing $\omega$-chains of approximations. At the same time one generates an order relation $\leq$ with constructors expressing that it is a preorder with bottom and suprema of increasing $\omega$-chains: $$\begin{aligned} \dfrac{}{x \leq x} \qquad \dfrac{x \leq y \qquad y \leq z}{x \leq z} \quad \dfrac{}{\bot \leq x} \dfrac{c : \omega\text{-}\mathrm{Chain}(A_\bot) \qquad i : \mathbb{N}}{c_i \leq \bigsqcup c} \qquad \dfrac{c : \omega\text{-}\mathrm{Chain}(A_\bot) \qquad (\forall i : \mathbb{N}.\; c_i \leq x)}{\bigsqcup c \leq x} \end{aligned}$$ Equality is generated by antisymmetry: $$\dfrac{x \leq y \qquad y \leq x}{x = y}$$ This presents $A_\bot$ as the free partiality object generated by $A$: values embed via $\eta$, divergence is represented by $\bot$, and non-terminating or approximating computations are built by increasing joins. ## Remarks For $A = \top$, one obtains the [[Sirpinski space]]. ## Monad structure The unit of the [[Monad|monad]] is the embedding $$\eta : A \to A_\bot.$$ The bind operation is not defined by pattern matching on explicit `later` constructors. Instead, it is obtained from the elimination principle or initiality of the QIIT presentation. This is one of the advantages of the direct construction: the monad structure is specified extensionally from the start, rather than being defined on representatives and then proved to respect a quotient. ## Relation to the delay monad The [[Delay Monad|delay monad]] is closely related, but it is not the same construction. - The delay monad is intensional: distinct finite delay patterns remain distinct. - The partiality monad is extensional: it identifies computations with the same observable partial behaviour. In extensional or set-theoretic settings, one often says that the partiality monad is the delay monad quotiented by weak bisimilarity. This is a useful intuition, but it is not the right direct definition in intensional type theory, because operations such as bind must be shown to respect the quotient. The QIIT presentation avoids this problem. ## References [[capretta2005-partiality]] [[altenkirch2017-partiality]] [[Quotient Inductive-Inductive Type]]