bernerbrau/Monads.md

## Monads.md

      
    Raw
  

              Monads.md
            
          
    Monad

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

There exists a function unit of type X → M[X]
There exists a function bind of type (M[X], X → R) → R
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]):

let unit(t:T) ≡ t
let bind(t:T,f:T → R) ≡ f(t)
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[()]:

let unit(u:Unit) ≡ unit(()) ≡ unit() ≡ ()
let bind(u:Unit, f:Unit → R) ≡ bind((), f:() → R) ≡ bind(f:() → R) ≡ f()
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(a:A) is a value of type T[A] and T(x) is a value of type T[X].
Definition. Define a type Box[X], such that:

box(x:X):Box[X] ≡ Box(x).
unbox(Box(x:X), f:X → R) ≡ f(x).
map(Box(x:X), f:X → R) ≡ Box(f(x)).


Notes

Here we see a monad that does something, namely, boxing and unboxing, but also, mapping.
Now, I didn't use the required Monad nomenclature. If you want to get picky, let's do that now.

unit(x:X):Box[X] ≡ box
bind(Box(x), f:X → R) ≡ unbox

As you can see, box and unbox are aliases for unit and bind, allowing the semantics of unit and bind to become clear.
But wait - we also used bind to create a third function. What?? Oh, I tricked you. Here, let's do a bit of substitution:
map(Box(x), f:X → R) ≡ map(bx:Box[X], f:X → R) ≡ box(unbox(bx,f)) ≡ unit(bind(bx,f))
bind turns out to be useful to create higher order abstractions.
Box also illustrates that the names for unit and bind aren't necessarily important (although having a common supertype M[X] allows for some really slick abstractions...) as long as the Monad structure and contract are honored.
Lastly let's go ahead and prove that Box is a monad:
Proof: Let type R, a:T and f:T → R. Then, bind(unit(a),f) ≡ unbox(box(a),f) ≡ unbox(Box(a),f) ≡ f(a).

A couple more monads that we'll want to use.

Eval

Definition. Define Eval[X] ≡ () → X.

unit(x:X):Eval[X] ≡ () → x.
bind(e:Eval[X], f:X → R) ≡ f(e()).
Proof:_ Let type R, a:T and f:T → R. Then, bind(unit(x),f) ≡ bind(() → a,f) ≡ f((() → a)()) ≡ f(a).


Notes

Eval works like Box, but there is an intermediate evaluation stage.
This could be useful if computing something is expensive, but we are also
building up to monads that allow for side effects.
Note the implementation of bind here!! Up until now bind has just been passing x to f. The flexibility of this abstraction begins to unfold.
What happens if we apply the definition of map over Box to Eval? Recall:
map(bx:Box[X], f:X → R) ≡ box(unbox(bx,f)) ≡ unit(f(bind(bx))
So:
map(ex:Eval[X], f:X → R) ≡ unit(bind(ex,f)) ≡ () → f(ex())
Interesting. Let's suspend mathematical purity for a minute and try something.
map(() → 10, x:int → x + 10) ≡ () → (() → 10)() + 10 ≡ () → 20
Look at what happened. For Eval, map does not immediately evaluate the underlying monad. Instead, it gives you a new (recursive -- in real life, check your language for tail call optimization!!) unevaluated Eval that, when evaluated, evaluates the underlying Eval and applies the mapping function. Cool!

Maybe

Definition. Given types T and U, then T | U is a union type over T and U.
Axiom. Given types S, T, U, if T⊆S and U⊆S then T|U ⊆ S.
Definition. Define Maybe[X] ≡ Box[X] | Unit.

Notes

Maybe is like nullables in OOP, but without the horrors of NullPointerException.
map is defined over Box, but not over Unit. Let's fix this.

map((), f:() → R) ≡ ()

Why did we do that? Well, because that's what we want Maybe to do if there's nothing in it. BUT! Let's take the definition of map over Box and see what happens when we apply it to Unit.

map(Box(x:X), f:X → R) ≡ Box(f(x)).
map((), f:X → R) ≡ ().

Note that X and R becomes unbound here, but that's OK because we're not using them anyway. In fact, we don't even care about f here, so let's drop it:
map(()) ≡ ().
Which simplifies further to:
map() ≡ ().
But that's confusing. In fact, we're using map so much, let's just promote it so it applies to all monads (hoping that it doesn't bite us later!):
Definition. map(a:A[X]⊆M[X], f:X→R):A[R] ≡ unit(bind(a,f))
And so, applying it to Unit:
map(a:Unit, f: Unit→R):Unit ≡ ()
All right, what's all this for? Well, Box and Unit are already defined for us. So, with our new universal map definition and our existing definitions of Box and Unit, we get this:


unit(u:Unit):Unit ≡ ()


bind(u:Unit, f:() → R):R ≡ f()


map(u:Unit, f:() → R):Unit ≡ ()


unit(x:X):Box[X] ≡ Box(x)


bind(Box(x:X), f:X → R):R ≡ f(x)


map(Box(x:X), f:X → R):Box[R] ≡ Box(f(x))


Recalling our definition, Maybe can be Unit (nothing) or a Box of something. So, map-ing a Maybe converts its value if it contains something, and leaves it unchanged if it doesn't.
Examples:


map((), x:string→parseInt(x)) ≡ ()
map(Box("123"), x:string→parseInt(x)) ≡ Box(123)

But let's look at bind for a second. What does it mean to bind a Maybe? Let's take a look. First, the combined binding function for Maybe has the signature:
bind(m:Unit|Box(X), f:(Unit|X)→R):R
Again, let's drop the mathematical purity and look at some examples.

bind((), ()→"Empty"|i:int→string(i)) ≡ "Empty"
bind(Box(123), ()→"Empty"|i:int→string(i)) ≡ "123"

So, quite by accident, binding a Maybe allows you to compute something based on its value, OR ELSE return a default. Let's define a convenience function for that:

let default((),d:X) ≡ bind((), ()→d|x:X→x)≡ bind((), ()→d) ≡ d
let default(Box(x:X),d:X) ≡ bind(Box(x:X), ()→d|x:X→x) ≡ bind(Box(x:X), x:X→x) ≡ x

NOTE: I've snuck in pattern matching here. I'm too lazy to formalize it.
It's important to note that calling bind directly permitted us to inject default behavior into a Maybe, and that it is not the whole semantics of bind over a maybe. map is also built on bind. Using these semantics you could say that map-ing a Maybe maps its value if it has one, OR ELSE returns (), but while this is an intuitive description, it's important to intuit how this occurs via the use of monadic binding.

Lists!

Let's try to define a List monad.
Definition. List[X] ≡ Unit | (X, List[X])

let unit(t:X) ≡ (t, ())
let bind((head:X, tail:List[X]),f:X → R):R ≡ ???!!!


Notes

Oh crap! What does it mean to bind a List??
Well, first, let's work from the constraint we have:
bind(unit(x),f) ≡ f(x)
So, bind((head:X, tail:Unit),f:X → R):R ≡ f(head). So we know what it means to bind a List with a single element,
but what about multiple elements?
It's easy to guess intuitively what map looks like on a List. Maybe we can work backwards:
map((head:X, tail:List[X]),f:X → R):List[R] ≡ (f(head), map(tail,f))
And our definition of map for monads:

map(a:A[X]⊆M[X], f:X→R):A[R] ≡ unit(bind(a,f))
So: (f(head), map(tail,f)) ≡ unit(bind((head,tail),f)) ≡ (bind((head,tail),f), ())
So: f(head) ≡ bind((head,tail),f) and map(tail,f) ≡ ().
So: bind((head,tail),f) ≡ f(head) and tail ≡ ()

This implies that the above definition of List can only be a monad if it contains a single element! Despair!
What else can we try? Well, let's assume we have an insufficient definition of map from back when we were working with single elements. Then what? Well, working from intuition, to have any kind of sensible list monad, we have to bind the rest of the list and combine the results somehow:
bind((head:X,tail:List[X]),f:X→R):R ≡ combine(f(head),bind(tail,f))
Hrm, maybe. We don't know what combine means, but at least we know it has signature (R,R)→R.
Rather than guess, let's leave the definition of combine open, currying it into bind and see where that gets us.

let bind:((R,R)→R)→(List[X],X→R)→R
let map:((R,R)→R)→(List[X],X→R)→List[R]