Option type
In programming languages (more so 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 (named None or Nothing), or which encapsulates the original data type A (written Just A or Some A). Outside of functional programming, these are termed nullable types.
In different programming languages, the option type has various names and definitions.
In type theory, it may be written as: .
In languages having tagged unions, as in most functional programming languages, option types can be expressed as the tagged union of a 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 one or zero elements.
The option type is a monad under these functions:
...
Wikipedia