By Jacob Neumann, June 2021
option is a SML datatype for handling potential undefined values. Formally, the option type is parametrized by a single polymorphic type variable, so for every SML type
t, there is a type
t option represents the construction of "either a value of
t, or nothing". For instance, a value of type
bool option is either true, false, or neither. A value of type
int option is either some integer, or none. A function will return
t option to represent the possibility that no acceptable value of type
t can be identified to return, and have a value to return to signal this circumstance. See the "Options-as-partiality" HOFs section below for some functions elaborating on this understanding of options.
Options also function as a kind of "container": a value
x : t option either "contains" a value of type
x = SOME(z)) or is an "empty container" with no values (
x = NONE). We can therefore view
t option as a degenerate version of
t list, where the "list" is constrained to be length at most one. The notion of a "container" is made precise in functional programming with the idea of a "monad". In Haskell (which makes much more explicit use of monads), options are known as the "Maybe monad".
t option has exactly one more value than the type
t itself. Formally,
datatype 'a option = NONE | SOME of 'a
So for each value
v : t,
SOME(v) : t option. And
NONE is a value of type
t option for each type
t, as required by the surrounding context. Options can be nested, e.g.
SOME(SOME(3)) : int option option.
NONE are the two constructors of the
t option type, so, in addition to the constructs generally available in pattern matching (e.g. wildcards and identifier binding), we can pattern match against
fun defaultToThree (NONE : int option):int = 3 | defaultToThree (SOME x) = x val 2 = defaultToThree(SOME 2) val 3 = defaultToThree(NONE) fun searchForEven  = NONE | searchForEven (x::xs) = if (x mod 2)=0 then SOME(x) else searchForEven xs val (SOME _) = searchForEven [1,2,3,4] val NONE = searchForEven [1,3,5]
t is pretty-printed by the
smlnj REPL (like
string list, etc.), so too is
t option. This is demonstrated by the following
smlnj REPL snippet.
- val k = SOME(SOME 5); val k = SOME (SOME 5) : int option option
There are some basic SML functions which produce
Int.fromString : string -> int option Bool.fromString : string -> bool option
Both of these functions are partial inverses to their respective
toString functions (e.g.
Int.fromString(Int.toString(7)) == SOME 7), but return an option so they can return
NONE on strings which do not encode an
Another option for casing on options is the function (provided in the
Option structure - see below)
Option.getOpt : 'a option * 'a -> 'a
which behaves as follows:
Option.getOpt(SOME x,y) will evaluate to
Option.getOpt(NONE,y) will evaluate to
y. When writing functions operating on options, it is still generally preferable that you use clausal pattern matching to break into the "
SOME case" and "
NONE case", but there are situations where
Option.getOpt is an elegant solution.
Option structure also provides the "join" function
Option.join : 'a option option -> 'a option
Option structure (part of the SMLNJ basis) provides a number of useful utilities for working with
In addition to the datatype
option itself being available at top-level, the exception
is available at top-level as well.
Option structure provides
boolean-valued functions for detecting whether a given option value is
SOME, and for extracting values from
Option.isSome : 'a option -> bool Option.isNone : 'a option -> bool Option.valOf : 'a option -> 'a
Option.valOf NONE raises the exception
Option. NOTE: Do not use these fuctions in place of pattern-matching on an option value. Expressions like
if Option.isSome(X) then Option.valOf(X) else e2 are bad style.
Options are an instance of a more general structure in functional programming known as a monad. Accordingly, there are a number of higher-order functions which we can define on options. In particular,
option comes equipped with a map operation:
Option.map : ('a -> 'b) -> 'a option -> 'b option
which does what you might expect, given its type:
Option.map f (SOME x) evaluates to
Option.map f NONE produces
NONE. As usual with "map" functions, we generally require
f to be total.
Options, as a "container" of data, also admit a filtering operation:
Option.filter : ('a -> bool) -> 'a option -> 'a option
Which is implemented as
fun filter p = fn NONE => NONE | (SOME x) => if p(x) then SOME x else NONE
i.e. it "filters" out the value
x does not "satisfy"
p(x) == false). As usual with "filter" functions, we generally require
p to be total.
Option structure also provides a utility for "folding" an option:
Option.fold : ('a * 'b -> 'b) -> 'b -> 'a option -> 'b
which we might implement as
fun fold g z NONE = z | fold g z (SOME x) = g(x,z)
We often assume that
g is total. In certain situations, we also want the two arguments of
g to be the same type, and might assume that
g is "associative" (in the sense that
g(x,g(y,z)) == g(g(x,y),z) for all
x,y,z) or that
z is a "unit" for
g(x,z) == x == g(z,x) for all
As mentioned above, options provide a way to represent partial functions: a function
f : t1 -> t2 option can be thought of as a function which is defined on some inputs (
f(x) == SOME(z)) and not on others (
f(y) == NONE). The
Option structure provides several utilities consistent with this interpretation. First is composition of these "partial functions".
Option.compose : ('a -> 'c) -> ('b -> 'a option) -> 'b -> 'c option Option.composePartial : ('a -> 'c option) -> ('b -> 'a option) -> 'b -> 'c option
(Option.compose (g,f))(x) will return
f(x) == NONE, and will return
f(x) == SOME(y).
Option.composePartial will behave similarly, except it will return
g(y) in the
f(x) == SOME(y) case, since
g returns an option.
It also provides a "partial" version of its map function:
Option.mapPartial : ('a -> 'b option) -> 'a option -> 'b option