In programming languages and type theory, an option type or maybe type is a polymorphic type that represents encapsulation of an optional value. It consists of either an empty constructor (called None or Nothing), or a constructor encapsulating the original data type A (written Just A or Some A). It is used for functions which may or may not return a meaningful value when they're applied.

PropertyValue
dbpprop:abstract
  • In programming languages and type theory, an option type or maybe type is a polymorphic type that represents encapsulation of an optional value. It consists of either an empty constructor (called None or Nothing), or a constructor encapsulating the original data type A (written Just A or Some A). It is used for functions which may or may not return a meaningful value when they're applied. In Haskell syntax, the option type (called Maybe) is defined as data Maybe a = Just a | Nothing In type theory, it may be written as: <math>A^{?} = A + 1</math>. In languages that have discriminated unions, as in most functional programming languages, option types can be expressed as the union of an unit type plus the encapsulated type. In the Curry-Howard correspondence, option types are related to the annihilation law for ∨: x∨1=1. An option type can also be seen as a collection containing either a single element or zero elements. The option type is a monad under the following functions: <math>\mathrm{return}\colon A \to A^{?} = a \mapsto \mathrm{Just} \, a</math> <math>\mathrm{bind}\colon A^{?} \to (A \to B^{?}) \to B^{?} = a \mapsto f \mapsto \begin{cases} \mathrm{Nothing} & \mbox{if } a = \mathrm{Nothing}\\ f \, a' & \mbox{if } a = \mathrm{Just} \, a' \end{cases}</math> We may also describe the option monad in terms of functions return, fmap and join, where the latter two are given by: <math>\mathrm{fmap} \colon (A \to B) \to (A^{?} \to B^{?}) = f \mapsto a \mapsto \begin{cases} \mathrm{Nothing} & \mbox{if } a = \mathrm{Nothing}\\ \mathrm{Just} \, f \, a' & \mbox{if } a = \mathrm{Just} \, a' \end{cases}</math> <math>\mathrm{join} \colon {A^{?}}^{?} \to A^{?} = a \mapsto \begin{cases} \mathrm{Nothing} & \mbox{if } a = \mathrm{Nothing}\\ \mathrm{Nothing} & \mbox{if } a = \mathrm{Just} \, \mathrm{Nothing}\\ \mathrm{Just} \, a' & \mbox{if } a = \mathrm{Just} \, \mathrm{Just} \, a' \end{cases}</math> The option monad is an additive monad: it has Nothing as a zero constructor and the following function as a monadic sum: <math>\mathrm{mplus} \colon A^{?} \to A^{?} \to A^{?} = a_1 \mapsto a_2 \mapsto \begin{cases} \mathrm{Nothing} & \mbox{if } a_1 = \mathrm{Nothing} \and a_2 = \mathrm{Nothing}\\ \mathrm{Just} \, a'_2 & \mbox{if } a_1 = \mathrm{Nothing} \and a_2 = \mathrm{Just} \, a'_2 \\ \mathrm{Just} \, a'_1 & \mbox{if } a_1 = \mathrm{Just} \, a'_1 \end{cases}</math> In fact, the resulting structure is an idempotent monoid.
rdfs:comment
  • In programming languages and type theory, an option type or maybe type is a polymorphic type that represents encapsulation of an optional value. It consists of either an empty constructor (called None or Nothing), or a constructor encapsulating the original data type A (written Just A or Some A). It is used for functions which may or may not return a meaningful value when they're applied.
rdfs:label
  • Option type
skos:subject
foaf:page
is dbpprop:redirect of