Definition
The maybe type of a type is the type of optional elements of . It contains either a value of type or a distinguished empty case.
In symbols:
with introduction rules
\dfrac{x : A}{\mathrm{just}(x) : \mathrm{Maybe}(A)} \qquad \dfrac{}{\mathrm{nothing} : \mathrm{Maybe}(A)} \end{aligned}$$ The type $\mathrm{Maybe}(A)$ is equivalent to the [[Sum Type|sum type]] $\mathbf{1} + A$. ## Eliminator To define a dependent function out of $\mathrm{Maybe}(A)$, it is enough to give: - a term for the `nothing` case - a term for the `just` case More formally, if $$P : \mathrm{Maybe}(A) \to \mathrm{Set}$$ and we have terms $$n : P(\mathrm{nothing})$$ and $$j : (x : A) \to P(\mathrm{just}(x)),$$ then there is an [[Eliminator|eliminator]] $$\mathrm{elim}_{\mathrm{Maybe}} : (m : \mathrm{Maybe}(A)) \to P(m).$$ It is determined by the computation rules $$\mathrm{elim}_{\mathrm{Maybe}}(\mathrm{nothing}) = n$$ and $$\mathrm{elim}_{\mathrm{Maybe}}(\mathrm{just}(x)) = j(x).$$ In non-dependent form, this is ordinary case analysis on an optional value. ## Related Concepts - [[Sum Type]] - [[Type Constructor]] - [[Partial Function]]