monad

We can abstract common part of language features such as state and exception. It allows programming these features in pure lambda calculus.

A monad \(M a\) is an abstract type—

the “normal” type is \(a\), and we have the semantics hidden in \(M\).

• return: \(a \to Ma\)
• bind: \(M a \to (a \to M b) \to M b\) — it takes a monad, a function that takes the unwrapped thing and hands back a new monad, and returns that

bind is written with \(v \gg = f\) for monad \(v\) and function \(f: a\to M b\)

discussion

Monads were used to explain stuff like state within Church theories; so languages are “core functional parts with monadic exceptions”—there’s a set of monads which is built in, like state, exceptions, concurrencies, ec.

upsides

• “just programming”: users can write their own monads
• fairly ubiquitous in haskall

downsides

• programs using return and bind tends to be contagious
• performance is bad: no free lunch
• stuff ends up looking like C++

state monad

• return: a -> Ma = \(\lambda v. \lambda s . (v,s)\) (just give us the state transformer)
• p >>= f: Ma -> (a -> Mb) -> Mb = \(\lambda s . let (v, s’) = (p\ s)\ \text{in}\ f\ v\ s’\)

“run p first against some state, get new state s’ and resulting value, then apply this value to \(f\), and then run it on the new state; notice that this whole thing takes a state”

exceptions

Exceptional e a =
  Success a |
  Exception e

the monad:

monad M  = Exceptional e

return := Success

bind:

>>= :: M a -> (a -> M b) -> M b
v >>= f = case v of
  Exception I -> Exception I
  Success r -> f r

throw:

throw = Exception

catch:

catch e h = case e of
  Exception I -> h I
  Success r -> Success r

partial functions

\(Maybe(a)\), that is Option

• head: List(a) -> Maybe(a)
• div: int -> int -> Maybe(int)

because these things may fail r not exist.

Maybe a =
  Just a |
  Nothing

Composition:

lx.let y = f x in
  case y of
    Nothing: Nothing
    Just v: g(v)

Notice how the above is tedious. We will then make this a monad.

monad M = Maybe

return: Just

bind

with \(v: Ma\), \(f: a \to Mb\)

v >>= f = case v of
  Nothing -> Nothing
  Just x -> f x

which means that we can write the above function:

lx.x >>= f >>= g

head of list

head x = case x of
  Nil: Nothing
  Cons(a,as): Just(a)

taking the head of the head of the list

λ l. return l >>= head >>= head