Monads (draft please ignore this for now)

4/4/18 draft


Monads are a topic of interest in functional programming, especially with functional programming languages like Haskell. Mathematicians would locate the idea or theory of monads as being within category theory.

The basic idea or conceptualization of monads is not too hard. There is the notion of wrapping a value, and the notion of binding which converts one wrapped value to another wrapped value. Wrapping is a function which takes one argument, the value, and wraps it. Of course, a wrapped value can be unwrapped and that would yield the value. Binding is a function that takes two arguments— one is a wrapped value, and the other is a function from a value to a wrapped value— and what binding does is to unwrap the value from the supplied wrapped value, apply the function to it, and return, the same or different, wrapped value.  Then there can be a sequence of binds, and these will just step from wrapped value to wrapped value.

What has just been explained is the abstraction of monads. Of course, there are many functions that could be used with bind (and, indeed, many functions that could be used to wrap). All of these would be, or might be, concrete examples of monads.

Monads can be illustrated or simulated with lambda calculus. However, there is a caution that might be given. Most modern functional programming languages are typed (that is, the values, the arguments, the functions all have types e.g. Integer, Integer=>Boolean, etc.). but the lambda calculus here is type free.

Wrapping and monadic value

For some of the following constructions, we would have liked to have used lambda abstractions without variables, but lambda calculus does not have these. Instead we will simulate this effect by using a variable which does not occur in the scope of the abstraction, and then, for applications, to use a dummy argument. The pattern is like this


and when that is called

     (λx.scopeWithNoX dummy)

it reduces to


A monadic value is a lambda abstraction, or closure over that value, so a monadic value is an abstraction (a function).

So monadic value corresponds to


and when that is called

     (λx.value dummy)

it reduces to


So the wrap function takes you from a value to the corresponding monadic value

     value to λx.value

and calling that function, with any argument, takes you back.

An example 'wrap' function which returns a monadic value is


or, for clarity, 


which when applied to



     (λvalue.λx.value valueToBeWrapped)

reduces to 



Bind takes a monadic value, and a function which produces a monadic value, and returns a monadic value

     (>>=)            :: m a -> (a -> m b) -> m b

a) monadic value


b) a function which returns a monadic value


(λy.λx.y value2) reduces to λx.value2

c) what bind does is the get the value1 out of the first monadic value1, apply the function to that value1 to get value2 then return monadic value2

     (λx.value1 dummy) // gets value1 out

     ((λy.λx.y value2) (λx.value1 dummy)) // applies the function to it

     λx.((λy.λx.y value2) (λx.value1 dummy)) // wrap that back into a monadic value

works in SoftOption!

((λv.λu.(u v) λx.a) λy.λx.y)


(λu.(u λx.a) λy.λx.y)


(λy.λx.y λx.a)



 ((λv.λu.(v u) λx.a) λy.λx.y)