Winter's formula

2013-12-12T21:52:36Z

155.99.204.81:

{{single source|date=June 2013}}
{{for|families of option contracts in finance|Option style}}

In [[programming language]]s (especially [[functional programming]] languages) and [[type theory]], an '''option type''' or '''maybe type''' is a [[parametric polymorphism|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 either an empty constructor (called ''None'' or ''Nothing''), or a constructor encapsulating the original data type A (written ''Just'' A or ''Some'' A). Outside of functional programming, these are known as [[nullable type]]s.

In the [[Haskell programming language|Haskell]] language, the option type (called ''Maybe'') is defined as <code>data Maybe a = Just a | Nothing</code>. In the [[OCaml]] language, the option type is defined as <code>type 'a option = None | Some of 'a</code>. In the [[Scala_(programming_language)|Scala]] language, [http://www.scala-lang.org/api/current/scala/Option.html Option] is defined as parametrized abstract class <code> '.. Option[A] = if (x == null) None else Some(x)..</code>. In the [[Standard ML]] language, the option type is defined as <code>datatype 'a option = NONE | SOME of 'a</code>. In the [[Rust (programming language)|Rust]] language, it is defined as <code>enum Option<T> { None, Some(T) }</code>.

In [[type theory]], it may be written as: <math>A^{?} = A + 1</math>.

In languages that have [[tagged union]]s, 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 [[absorption law|annihilation law]] for ∨: x∨1=1.

An option type can also be seen as a [[collection (computing)|collection]] containing either a single element or zero elements.

== The option monad ==
The option type is a [[monads in functional programming|monad]] under the following functions:
:<math>\text{return}\colon A \to A^{?} = a \mapsto \text{Just} \, a</math>
:<math>\text{bind}\colon A^{?} \to (A \to B^{?}) \to B^{?} = a \mapsto f \mapsto \begin{cases} \text{Nothing} & \text{if} \ a = \text{Nothing}\\ f \, a' & \text{if} \ a = \text{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>\text{fmap} \colon (A \to B) \to A^{?} \to B^{?} = f \mapsto a \mapsto \begin{cases} \text{Nothing} & \text{if} \ a = \text{Nothing}\\ \text{Just} \, f \, a' & \text{if} \ a = \text{Just} \, a' \end{cases}</math>
:<math>\text{join} \colon {A^{?}}^{?} \to A^{?} = a \mapsto \begin{cases} \text{Nothing} & \text{if} \ a = \text{Nothing}\\ \text{Nothing} & \text{if} \ a = \text{Just} \, \text{Nothing}\\ \text{Just} \, a' & \text{if} \ a = \text{Just} \, \text{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>\text{mplus} \colon A^{?} \to A^{?} \to A^{?} = a_1 \mapsto a_2 \mapsto \begin{cases} \text{Nothing} & \text{if} \ a_1 = \text{Nothing} \and a_2 = \text{Nothing}\\ \text{Just} \, a'_2 & \text{if} \ a_1 = \text{Nothing} \and a_2 = \text{Just} \, a'_2 \\ \text{Just} \, a'_1 & \text{if} \ a_1 = \text{Just} \, a'_1 \end{cases}</math>

In fact, the resulting structure is an [[idempotent]] [[monoid]].

== Examples ==

=== Scala ===
[[Scala (programming language)|Scala]] implements Option as a parameterized type, so a variable can be an Option, accessed as follows:<ref name="OderskySpoon2008">{{cite book|author1=Martin Odersky|author2=Lex Spoon|author3=Bill Venners|title=Programming in Scala|url=http://books.google.com/books?id=MFjNhTjeQKkC&pg=PA283|accessdate=6 September 2011|year=2008|publisher=Artima Inc|isbn=978-0-9815316-0-1|pages=282–284}}</ref>
<source lang="scala">
// Defining variables that are Options of type Int
val res1: Option[Int] = Some(42)
val res2: Option[Int] = None

// This function uses pattern matching to deconstruct Options
def compute(opt: Option[Int]) = opt match {
case None => "No value"
case Some(x) => "The value is: " + x
}

System.out.println(compute(res1)) // The value is: 42
System.out.println(compute(res2)) // No value
</source>

An Option value is usually used with [[pattern matching]], as in the previous example.
In this way, the program is safe as it cannot generate any exception or error (e.g. by trying to obtain the value of an <code>Option</code> variable that is equal to <code>None</code>).
Therefore, it essentially works as a type-safe alternative to the null value.

=== F# ===
<source lang="ocaml">

(* This function uses pattern matching to deconstruct Options *)
let compute = function
None -> "No value"
| Some x -> sprintf "The value is: %d" x

printfn "%s" (compute <| Some 42)(* The value is: 42 *)
printfn "%s" (compute None) (* No value *)
</source>

=== Haskell ===
<source lang="haskell">
-- Defining variables that are Maybes of type Int
res1, res2 :: Maybe Int
res1 = Just 42
res2 = Nothing

-- This function uses pattern matching to deconstruct Maybes
compute :: Maybe Int -> String
compute may = case may of
Nothing -> "No value"
Just x -> "The value is: " ++ show x

main = do
print $ compute res1 -- The value is: 42
print $ compute res2 -- No value
</source>

== See also ==
* [[Tagged union]]
* [[Nullable type]]
* [[Null Object pattern]]
* [[Sentinel value]]

== References ==
<references />

{{Data types}}

[[Category:Functional programming]]
[[Category:Data types]]
[[Category:Type theory]]

formulasearchengine - User contributions [en]

Winter's formula