Option type

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're 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).

In the Haskell language, the option type (called Maybe) is defined as data Maybe a = Just a | Nothing. In the OCaml language, the option type is defined as type 'a option = None | Some of 'a. In the Scala language, Option is defined as parametrized abstract class '.. Option[A] = if (x == null) None else Some(x)... In the Standard ML language, the option type is defined as datatype 'a option = NONE | SOME of 'a.

In type theory, it may be written as: A? = A + 1.

In languages that have discriminated unions (or sum types), as in most functional programming languages, option types can be expressed as the 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 a single element or zero elements.

Contents

The option monad

The option type is a monad under the following functions:

\text{return}\colon A \to A^{?} = a \mapsto \text{Just} \, a
\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}

We may also describe the option monad in terms of functions return, fmap and join, where the latter two are given by:

\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}
\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}

The option monad is an additive monad: it has Nothing as a zero constructor and the following function as a monadic sum:

\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}

In fact, the resulting structure is an idempotent monoid.

Examples

Scala

Scala implements the Option type using Java generics, so you can specify the type of a variable as an Option and then access it as follows:[1]

class Person(val name: String, val age: Int)
 
var mightBeAPerson: Option[Person] = None
 
mightBeAPerson.isDefined // false
 
mightBeAPerson = Some(Person("Fred Flintstone", 50))
 
mightBeAPerson.isDefined // true
 
mightBeAPerson.get // returns the object

It essentially works as a type-safe alternative to the null value.

See also

References

  1. ^ Martin Odersky; Lex Spoon; Bill Venners (2008). Programming in Scala. Artima Inc. pp. 282–284. ISBN 978-0-9815316-0-1. http://books.google.com/books?id=MFjNhTjeQKkC&pg=PA283. Retrieved 6 September 2011. 

Wikimedia Foundation. 2010.

Игры ⚽ Поможем сделать НИР

Look at other dictionaries:

  • Option — may refer to Contents 1 Legal rights 2 Sport 3 Computing 4 Publications 5 History …   Wikipedia

  • Option Margin — The cash or securities an investor must deposit in his account as collateral before writing options. Margin requirements vary by option type. Margin requirements are established by the Federal Reserve Board in Regulation T; individual brokers may …   Investment dictionary

  • Option (finance) — Option Une option est un produit dérivé, en finance de marché, qui donne le droit, lorsqu on l achète, ou l obligation, lorsqu on la vend, d acheter ou de vendre un actif financier à un prix fixé à l avance (strike) pendant un temps donné ou à… …   Wikipédia en Français

  • Option américaine — Option Une option est un produit dérivé, en finance de marché, qui donne le droit, lorsqu on l achète, ou l obligation, lorsqu on la vend, d acheter ou de vendre un actif financier à un prix fixé à l avance (strike) pendant un temps donné ou à… …   Wikipédia en Français

  • Option européenne — Option Une option est un produit dérivé, en finance de marché, qui donne le droit, lorsqu on l achète, ou l obligation, lorsqu on la vend, d acheter ou de vendre un actif financier à un prix fixé à l avance (strike) pendant un temps donné ou à… …   Wikipédia en Français

  • Option réelle — Option Une option est un produit dérivé, en finance de marché, qui donne le droit, lorsqu on l achète, ou l obligation, lorsqu on la vend, d acheter ou de vendre un actif financier à un prix fixé à l avance (strike) pendant un temps donné ou à… …   Wikipédia en Français

  • Type design — is the art of designing typefaces. Although the technology of printing text using movable type was invented in China, and despite the esteem which calligraphy held in that civilization, the vast number of Chinese characters meant that few… …   Wikipedia

  • Option Québec — Auteur René Lévesque et al. Genre Essai Pays d origine  Canada Lieu de parution Montréal, Québec …   Wikipédia en Français

  • Type system — Type systems Type safety Inferred vs. Manifest Dynamic vs. Static Strong vs. Weak Nominal vs. Structural Dependent typing Duck typing Latent typing Linear typing Uniqueness typing …   Wikipedia

  • Type de média internet — Type MIME Un Internet media type[1], à l origine appelé Type MIME ou juste MIME ou encore Content type[2], est un identifiant de format de données sur internet en deux parties. Les identifiants étaient à l origine définis dans la RFC 2046 pour… …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”