Examples of monads in a dynamic language

In Monads in dynamic languages, I explained what the definition of a monad in a dynamic language should be and concluded that there’s nothing precluding them from existing. But I didn’t give an example either.

So, in case you are still wondering whether non-trivial monads are possible in a dynamic language, here you go. I’ll implement a couple of simple monads — Reader and Maybe — with proofs.

And all that will take place in the ultimate dynamic language — the (extensional) untyped lambda calculus.

The definitions of the Reader and Maybe monads are not anything special; they are the same definitions as you would write, say, in Haskell, except Maybe is Church-encoded.

What I find fascinating about this is that despite the untyped language, which allows more things to go wrong than a typed one, the monad laws still hold. You can still write monadic code and reason about it in the untyped lambda calculus in the same way as you would do in a typed language.

Reader

return x = λr.x
a >>= k  = λr.k(ar)r

Left identity

return x >>= k
  { inline return }
  = λr.x >>= k
  { inline >>= }
  = λr.k((λr.x)r)r
  { β-reduce }
  = λr.kxr
  { η-reduce }
  = kx

Right identity

a >>= return
  { inline return }
  = a >>= λx.λr.x
  { inline >>= }
  = λr.(λx.λr.x)(ar)r
  { β-reduce }
  = λr.ar
  { η-reduce }
  = a

Associativity

a >>= f >>= g
  { inline 1st >>= }
  = λr.f(ar)r >>= g
  { inline 2nd >>= }
  = λr.g((λr.f(ar)r)r)r
  { β-reduce }
  = λr.g(f(ar)r)r

a >>= (λx. f x >>= g)
  { inline 2nd >>= }
  = a >>= λx.λr.g((fx)r)r
  { inline 1st >>= }
  = λr.(λx.λr.g(fxr)r)(ar)r
  { β-reduce }
  = λr.g(f(ar)r)r

Maybe

return x = λj.λn.jx
a >>= k  = λj.λn.a(λx.kxjn)n

Left identity

return x >>= k
  { inline return }
  = λj.λn.jx >>= k
  { inline >>= }
  = λj.λn.(λj.λn.jx)(λx.kxjn)n
  { β-reduce }
  = λj.λn.kxjn
  { η-reduce }
  = kx

Right identity

a >>= return
  { inline return }
  = a >>= λx.λj.λn.jx
  { inline >>= }
  = λj.λn.a(λx.(λx.λj.λn.jx)xjn)n
  { β-reduce }
  = λj.λn.a(λx.jx)n
  { η-reduce }
  = λj.λn.ajn
  { η-reduce }
  = a

Associativity

a >>= f >>= g
  { inline 1st >>= }
  = (λj.λn.a(λx.fxjn)n) >>= g
  { inline 2nd >>= }
  = (λj.λn.(λj.λn.a(λx.fxjn)n)(λx.gxjn)n)
  { β-reduce }
  = λj.λn.a(λx.fx(λx.gxjn)n)n

a >>= (λx. f x >>= g)
  { inline 2nd >>= }
  = a >>= (λx.λj.λn.fx(λx.gxjn)n)
  { inline 1st >>= }
  = λj.λn.a(λx.(λx.λj.λn.fx(λx.gxjn)n)xjn)n
  { β-reduce }
  = λj.λn.a(λx.fx(λx.gxjn)n)n