Maybe.fm

// Maybe.fm
// ========
// 
// Optional values. A value of type `Maybe(A)` can either be
// a value of type `A`, or nothing at all. Maybe captures
// the idea of "nullable" values, and functions that can
// fail to produce a result.

import Bool

// Definition
// ----------

T Maybe{A}
| none
| some(value : A)

// Operations
// ----------

maybe(A; B; b : B, f : A -> B, mb : Maybe(A)) : B
  case mb
  | none => b
  | some => f(mb.value)

is_some(A; mb : Maybe(A)) : Bool
  case mb
  | none => false
  | some => true

is_none(A; mb : Maybe(A)) : Bool
  case mb
  | none => true
  | some => false

with_default(A; x : A, mb : Maybe(A)) : A
  maybe(__ x, (x) => x, mb)

map_maybe(A; B; f : A -> B, mb : Maybe(A)) : Maybe(B)
  case mb
  | none => none(_)
  | some => some(_ f(mb.value))

apply_maybe(A; B; mf: Maybe(A -> B), mb : Maybe(A))
: Maybe(B)
  case mf
  | none => none(_)
  | some => map_maybe(A; B; mf.value, mb)

pure_maybe(A;): A -> Maybe(A)
  some(A;)

bind_maybe(A; B; f: A -> Maybe(B), mb: Maybe(A)) : Maybe(B)
  case mb
  | none => none(_)
  | some => f(mb.value)