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).
[1] In the Curry–Howard correspondence, option types are related to the annihilation law for ∨: x∨1=1.[how?]
[3] In Agda, the option type is named Maybe with variants nothing and just a.
In ATS, the option type is defined as Since C++17, the option type is defined in the standard library as template
[5] In Haskell, the option type is defined as data Maybe a = Nothing | Just a.
[8] In Scala, the option type is defined as sealed abstract class Option[+A], a type extended by final case class Some[+A](value: A) and case object None.
Payload n can be captured in an if or while statement, such as if (opt) |n| { ... } else { ... }, and an else clause is evaluated if it is null.