maybe monad

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** = **propositions as types** +**programs as proofs** +**relation type theory/category theory**

What is called the *maybe monad* is a simple monad (in computer science) which is used to implement “exceptions” indicating the failure of a computation in terms of functional programming.

On the type system the maybe monad is the operation $X \mapsto X \coprod \ast$.

The idea here is that a function $X \longrightarrow Y$ in its Kleisli category is in the original category a function of the form $X \longrightarrow Y \coprod \ast$ so either returns indeed a value in $Y$ or else returns the unique element of the unit type/terminal object $\ast$ – it is a *partial function*. The latter case is naturally interpreted as “no value returned”, hence as indicating a “failure in computation”.

under construction

The Kleisli category of the maybe monad on $Set$ is the category whose objects are sets, and whose morphisms are partial functions.

This observation generalizes as follows: if $\mathbf{C}$ is an extensive category and has a terminal object $\ast$, then a morphism $g: X \to Y \coprod \ast$ as an object of the overcategory $\mathbf(C)/(Y \coprod \ast)$ determines (uniquely up to canonical isomorphism) an object

$(f: X_1 \to Y, !: X_2 \to \ast) \in \mathbf{C}/Y \times \mathbf{C}/\ast$

such that $g = f \coprod !$, in other words a partial morphism $f: X \rightharpoonup Y$ whose domain of definition is a subobject $X_1 \hookrightarrow X$ with complement $X_2 \hookrightarrow X$. In brief, maps in the Kleisli category are partial maps with complemented domain.

In particular, in the case of a Boolean topos, the Kleisli category is the category of objects and partial maps; see also partial map classifier.

The algebras over the maybe monad are pointed objects.

Moreover, assuming $\mathbf{C}$ has finite products and an appropriate form of distributivity (which obtains if for example $\mathbf{C}$ is lextensive), the maybe monad on $\mathbf{C}$ is a monoidal monad on the cartesian monoidal category $\mathbf{C}$. It follows (by the discussion at *commutative monad*, see also (Seal 12)) that its Eilenberg-Moore category of algebras canonically inherits the structure of a monoidal category, at least under the mild assumption that it has reflexive coequalizers. Note that the maybe monad $T$ preserves reflexive coequalizers, so the monadic functor creates reflexive coequalizers if the base category has them; in this abstract setting the monoidal product on algebras $(X, \alpha: T X \to X)$, $(Y, \beta: T Y \to Y)$ is given explicitly as the coequalizer of $T(\alpha \times \beta): T(T X \times T Y) \to T(X \times Y)$ and

$T(T X \times T Y) \stackrel{T(\phi_{X, Y})}{\to} T T(X \times Y) \stackrel{\mu}{\to} T(X \times Y)$

where $\phi$ is one of the structural constraints on the monoidal monad $T$ and $\mu$ is the multiplication on $T$. One finds that this coequalizer yields the usual smash product of pointed objects.

The smash product as the correct monoidal product can also be deduced in a perhaps more perspicuous manner if we assume more of the base category: that it is cartesian closed, finitely complete, and finitely cocomplete. In that case we construct the internal hom of $T$-algebras, i.e., the internal hom of pointed objects $(Y, \beta: T Y \to Y)$ and $(Z, \gamma: T Z \to Z)$ directly as an equalizer of maps

$\array{
Z^Y & \to & T Z^{T Y} \\
& \mathllap{Z^\beta} \searrow & \downarrow \mathrlap{\gamma^{T Y}} \\
& & Z^{T Y}
}$

where the top arrow expresses enriched functoriality of $T$ (which in turn is closely related to the strength on $T$). The success of this is guaranteed by the commutativity of the monad (which here takes a particularly simple form, being given by the commutative *monoid* $\ast$ with respect to coproduct $\coprod$). Then, by taking the monoidal product that is adjoint to the internal hom, one is led to the smash product $(X \wedge Y)_\ast$ all the same: that is, one can read off the smash product from the fact that pointed maps $X_\ast \to \hom_\ast(Y_\ast, Z_\ast)$ should correspond to pointed maps $(X \wedge Y)_\ast \to Z_\ast$.

Regarding just the underlying endofunctor of the maybe monad, its initial algebra over an endofunctor is a natural numbers object.

- Gavin J. Seal,
*Tensors, monads and actions*(arXiv:1205.0101)

Around (0.4.24.2) in

- Nikolai Durov,
*New Approach to Arakelov Geometry*(arXiv:0704.2030)

the algebraic structure of the would be “field with one element” is regarded as being the maybe monad, hence modules over $\mathbb{F}_1$ are defined to be monad-algebras over the maybe monad, hence pointed sets.

Last revised on September 30, 2014 at 05:14:44. See the history of this page for a list of all contributions to it.