On Monads

Monads.md

Monad

A type T is a subtype of type M[X] iff:

1. There exists a function unit of type X → M[X]
2. There exists a function bind of type (M[X], X → R) → R
3. For all x:X and f:X→R : bind(unit(x),f) ≡ f(x)

Notes

The natural inclination is to ask, "What are the semantics here?" but it turns out that the semantics depend wholly on the type. The more monadic types we define, the clearer it will become how the above constraints are useful.

Simple Monad Types

Trivial

We can show that any type T has a trivially monadic structure (or: ∀T:T⊆M[T]):

1. let unit(t:T) ≡ t
2. let bind(t:T,f:T → R) ≡ f(t)
3. Proof: Let type R, a:T and f:T → R. Then, bind(unit(a),f) ≡ bind(a,f) ≡ f(a).

Therefore, ∀T:T⊆M[T]. QED.

Notes

So everything is a monad? What the hell? There is so much nuance to monads that it is hard to intuit them from a rigorous definition.

Unit

Definition. The Unit type is a type containing one member, denoted (), or the dimensionless tuple. Using the definition above, we show that () has type M[()]:

1. let unit(u:Unit) ≡ unit(()) ≡ unit() ≡ ()
2. let bind(u:Unit, f:Unit → R) ≡ bind((), f:() → R) ≡ bind(f:() → R) ≡ f()
3. Proof: Let type R and f:() → R. Then, bind(unit(()),f) ≡ bind((),f) ≡ bind(f) ≡ f().

Therefore, ()⊆M[()].

Box

Definition. Given type T[X] and x:X, then T(x) is a value of type T[X]. Definition. Define a type Box[X], such that:

1. box(x:X):Box[X] ≡ Box(x).
2. unbox(Box(x), f:Box[X] → R) ≡ f(x).
3. Proof: Let type R, a:T and f:T → R. Then, unbox(box(a),f) ≡ unbox(Box(a),f) ≡ f(a).