Option type

In programming languages (especially functional programming languages) and type theory, an option type or maybe type is a polymorphic type that represents encapsulation of an optional value; e.g., it is used as the return type of functions which may or may not return a meaningful value when they are applied. It consists of a constructor which either is empty (often named None or Nothing), or which encapsulates the original data type A (often written Just A or Some A). A distinct, but related concept outside of functional programming, which is popular in object-oriented programming, is called nullable types (often expressed as A?). The core difference between option types and nullable types is that option types support nesting (e.g. Maybe (Maybe String) ≠ Maybe String), while nullable types do not (e.g. String?? = String?). In type theory, it may be written as: . This expresses the fact that for a given set of values in , an option type adds exactly one additional value (the empty value) to the set of valid values for . This is reflected in programming by the fact that in languages having tagged unions, option types can be expressed as the tagged union of the encapsulated type plus a unit 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 one or zero elements. The option type is also a monad where: return = Just -- Wraps the value into a maybe Nothing >>= f = Nothing -- Fails if the previous monad fails (Just x) >>= f = f x -- Succeeds when both monads succeed The monadic nature of the option type is useful for efficiently tracking failure and errors. In Agda, the option type is named with variants and . Since C++17, the option type is defined in the standard library as . In Coq, the option type is defined as . In Elm, the option type is defined as . let showValue = Option.