Ministry of higher and secondary public education of the republic of uzbekistan academic lyceum at the uzbek state university of world languages

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 Elm, it is named Maybe, and defined as type Maybe a = Just a | Nothing.^[4]
  
• 
  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 Python, it is denoted (via type hints) as typing.Optional[T], or T | None in 3.10 and above.
  
• 
  In Rust, it is defined as enum Option { 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 { case none, some(T) } but is generally written as T?.^[5]
  

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: