librarylib/Maybe.xtl

Maybe: a value that may be missing, and the monad that chains computations which can fail (a standard library, built into xetal). Import it with an alias of your choice: "m:" u_se< "Maybe".

A maybe is Church-encoded: it is a function of two arguments, what to give when it is empty and what to do with its value. n_othing gives the first; j_ust x applies the second to x.

Like '+ r_/ A, the function comes first, as a quoted operand, so a chain reads right to left: 'g b_ind 'f b_ind m is f, then g.

source

Making a maybe

ˡn̲othing : a -> b -> a

function · line 18

The empty maybe.

      ᵐ⁼u̲se< "Maybe"

      0 ᵐo̲r 'ᵐn̲othing
0

ˡn̲othing ← { n j → n }

Used in: ˡm̲ap, ˡb̲ind

ˡj̲ust : a -> b -> (a -> c) -> c

function · line 24

A maybe holding x.

      ᵐ⁼u̲se< "Maybe"

      0 ᵐo̲r ᵐj̲ust 7
7

ˡj̲ust ← { x n j̲ → j̲ x }

Used in: ˡm̲ap

Using a maybe

ˡm̲aybe : a -> b -> (b -> a -> c) -> c

function · line 29

d 'f m_aybe m: f applied to m's value, or d when m is empty.

ˡm̲aybe ← { f̲ d m̲ → d m̲ 'f̲ }

ˡo̲r : a -> (a -> (b -> b) -> c) -> c

function · line 32

d o_r m: m's value, or d when m is empty.

ˡo̲r ← { d m̲ → d m̲ '{ x → x } }

ˡm̲ap : (a -> b) -> ((c -> d -> c) -> (a -> e -> (b -> f) -> f) -> g) -> g

function · line 35

'f m_ap m: f applied inside the maybe; empty stays empty.

ˡm̲ap ← { f̲ m̲ → 'ˡn̲othing m̲ '{ x → ˡj̲ust f̲ x } }

ˡb̲ind : a -> ((b -> c -> b) -> a -> d) -> d

function · line 39

'f b_ind m: f (which gives a maybe) applied to m's value; empty stays empty, so a chain of steps stops at the first that fails.

ˡb̲ind ← { f̲ m̲ → 'ˡn̲othing m̲ 'f̲ }