# 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 (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 (`Maybe (Maybe A)`

≠ `Maybe A`

), while nullable types do not (`String??`

= `String?`

).

## Contents

## Theoretical aspects

}}

In type theory, it may be written as: [math]A^{?} = A + 1[/math]. This expresses the fact that for a given set of values in [math]A[/math], an option type adds exactly one additional value (the empty value) to the set of valid values for [math]A[/math]. 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.^{[1]}

In the Curry–Howard correspondence, option types are related to the annihilation law for ∨: x∨1=1.

The option type is also a monad where:^{[2]}

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.^{[3]}

## Names and definitions

In different programming languages, the option type has various names and definitions.

- In Agda, it is named
`Maybe`

with variants`nothing`

and`just a`

. - In Coq, it is defined as
`Inductive option (A:Type) : Type := | Some : A -> option A | None : option A.`

. - In Haskell, it is named
*Maybe*, and defined as`data Maybe a = Nothing | Just a`

. - In Idris, it is defined as
`data Maybe a = Nothing | Just a`

. - In OCaml, it is defined as
`type 'a option = None | Some of 'a`

. - In Rust, it is defined as
`enum Option<T> { None, Some(T) }`

. - In Scala, it is defined as
`sealed abstract class Option[+A]`

, a type extended by`final case class Some[+A](value: A)`

and`case object None`

. - In Standard ML, it is defined as
`datatype 'a option = NONE | SOME of 'a`

. - In Swift, it is defined as
`enum Optional<T> { case none, some(T) }`

but is generally written as`T?`

.

## Examples

### Ada

Ada does not implement option-types directly, however it provides discriminated types which can be used to parameterize a record. To implement a Option type, a Boolean type is used as the discriminant; the following example provides a generic to create an option type from any non-limited constrained type:

Generic -- Any constrained & non-limited type. Type Element_Type is private; Package Optional_Type is -- When the discriminant, Has_Element, is true there is an element field, -- when it is false, there are no fields (hence the null keyword). Type Optional( Has_Element : Boolean ) is record case Has_Element is when False => Null; when True => Element : Element_Type; end case; end record; end Optional_Type;

### Scala

Scala implements `Option`

as a parameterized type, so a variable can be an `Option`

, accessed as follows:^{[4]}

// Defining variables that are Options of type Int val res1: Option[Int] = Some(42) val res2: Option[Int] = None // sample 1 : 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 } // sample 2 : This function uses built-in fold method def compute(opt: Option[Int]) = opt.fold("No value")(v => "The value is: " + v ) println(compute(res1)) // The value is: 42 println(compute(res2)) // No value

Two main ways to use an `Option`

value exist. The first, not the best, is the pattern matching, as in the first example. The second, the best practice is a monadic approach, as in the second example. In this way, a program is safe, as it can generate no exception or error (e.g., by trying to obtain the value of an `Option`

variable that is equal to `None`

). Thus, it essentially works as a type-safe alternative to the null value.

### OCaml

OCaml implements `Option`

as a parameterized variant type. `Option`

s are constructed and deconstructed as follows:

(* Deconstructing options *) let compute opt = match opt with | None -> "No value" | Some x -> "The value is: " ^ string_of_int x print_endline (compute None) (* "No value" *) print_endline (compute (Some 42)) (* "The value is: 42" *)

### F#

(* 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 *)

### Haskell

-- This function uses pattern matching to deconstruct Maybes compute :: Maybe Int -> String compute Nothing = "No value" compute (Just x) = "The value is: " ++ show x main :: IO () main = do print $ compute (Just 42) -- The value is: 42 print $ compute Nothing -- No value

### Swift

func compute(_ x: Int?) -> String { // This function uses optional binding to deconstruct optionals if let y = x { // y is now the non-optional `Int` content of `x`, if it has any return "The value is: \(y)" } else { return "No value" } } print(compute(42)) // The value is: 42 print(compute(nil)) // No value

### Rust

fn main() { // This function uses pattern matching to deconstruct optionals fn compute(x: Option<i32>) -> String { match x { Some(a) => format!("The value is: {}", a), None => format!("No value"), } } println!("{}", compute(Some(42))); // The value is: 42 println!("{}", compute(None)); // No value }

### Nim

import options #Module must be imported proc compute(a : Option[int])= if(a.isSome): echo "The Value is: " & $a.get else: echo "The Value is None" var a : Option[int] = option(42) b : Option[int] compute(a) #The Value is: 42 compute(b) #The Value is None

## See also

## References

- ↑ Milewski, Bartosz (2015-01-13). "Simple Algebraic Data Types" (in en). Sum types. "We could have encoded Maybe as: data Maybe a = Either () a". https://bartoszmilewski.com/2015/01/13/simple-algebraic-data-types/.
- ↑ "A Fistful of Monads - Learn You a Haskell for Great Good!". http://www.learnyouahaskell.com/a-fistful-of-monads.
- ↑ Hutton, Graham (Nov 25, 2017). "What is a Monad?". https://www.youtube.com/watch?v=t1e8gqXLbsU.
- ↑ Martin Odersky; Lex Spoon; Bill Venners (2008).
*Programming in Scala*. Artima Inc. pp. 282–284. ISBN 978-0-9815316-0-1. https://books.google.com/books?id=MFjNhTjeQKkC&pg=PA283. Retrieved 6 September 2011.

Original source: https://en.wikipedia.org/wiki/ Option type.
Read more |