Maybe Monad

Definition

The maybe monad or option monad is the monad on Set whose underlying endofunctor sends a set $A$ to the maybe type $\mathrm{Maybe}(A)\cong 1+A$.

Its unit is the map

$${\eta }_A:A\to \mathrm{Maybe}(A)$$

given by ${\eta }_A(x)=\mathrm{just}(x)$.

Its multiplication

$${\mu }_A:\mathrm{Maybe}(\mathrm{Maybe}(A))\to \mathrm{Maybe}(A)$$

flattens a nested optional value by sending $\mathrm{just}(\mathrm{just}(x))$ to $\mathrm{just}(x)$ and every other case to $\mathrm{nothing}$.

Kleisli Structure

Equivalently, for $x:\mathrm{Maybe}(A)$ and $g:A\to \mathrm{Maybe}(B)$, the Kleisli extension $x>>=g$ is defined to be $g(x_0)$ if $x=\mathrm{just}(x_0)$ and $\mathrm{nothing}$ if $x=\mathrm{nothing}$.

Partiality

The maybe monad represents a simple form of partiality in which definedness is decidable. It is the decidable instance of the lifting pattern.

Related Concepts

Lifting Monad
Maybe Type
Monad
Partiality (Type Theory)