Abstract

A type for signifing missing values.

Synopsis

type opt 'a = #none | #some a
val add_identity 'a : (op: a -> a -> a) -> (a: #none | #some a) -> (b: #none | #some a) -> opt a
val from_opt 'a : (ne: a) -> (a: #none | #some a) -> a
val map_opt 'a 'b : (f: a -> b) -> (x: #none | #some a) -> opt b
val equal_opt 'a : (eq: a -> a -> bool) -> (a: #none | #some a) -> (b: #none | #some a) -> bool
val some 'a : (a: a) -> opt a
val is_some 'a : (a: #none | #some a) -> bool
val is_none 'a : (a: #none | #some a) -> bool
val bind_opt 'a 'b : (f: a -> #none | #some b) -> (a: #none | #some a) -> opt b
val first_some 't [d₀] : (xs: [d₀]#none | #some t) -> opt t

Description

↑type opt 'a = #none | #some a
↑val add_identity 'a: (op: a -> a -> a) -> (a: #none | #some a) -> (b: #none | #some a) -> opt a

Extents a binary operation to have #none as a identity element.

This can be used when a associative operation has no neutral element.

↑val from_opt 'a: (ne: a) -> (a: #none | #some a) -> a

Unpacks an opt value.

If #some a then a is returned, otherwise ne is returned.

↑val map_opt 'a 'b: (f: a -> b) -> (x: #none | #some a) -> opt b

Maps a function inside opt.

Applies the function f to the value 'a.

↑val equal_opt 'a: (eq: a -> a -> bool) -> (a: #none | #some a) -> (b: #none | #some a) -> bool

Definition of a opt equality.

The equality holds if they are both #none or they are both #some and the values inside #some are equal.

↑val some 'a: (a: a) -> opt a

Maps a value to a opt type.

This is syntactic sugar for #some a, it may be nicer to use then a lambda function.

↑val is_some 'a: (a: #none | #some a) -> bool

is_some a is true if the constructor is #some.

↑val is_none 'a: (a: #none | #some a) -> bool

is_none a is true when constructor is #none.

↑val bind_opt 'a 'b: (f: a -> #none | #some b) -> (a: #none | #some a) -> opt b

The bind operation for the optional type.

↑val first_some 't [d₀]: (xs: [d₀]#none | #some t) -> opt t

Find the first #some element if one exists.