Monad Laws#

A monad has two combinators, ">>=" (bind) and "return" satisfying:

  1. Left identity: (return a) >>= ff a
  2. Right identity: m >>= return ≡ m
  3. Associativity: (m >>= f) >>= gm >>= (λx. f x >>= g)

Sequential Combinator#

If we write m >x> f(x) for m >>= f, and use let for "return", the monad laws are satisfied.

  1. Left identity: let(a) >x> f(x)f(a)
  2. Right identity: m >x> let(x)m
  3. Associativity: (m >x> f(x)) >y> g(y)m >x> (f(x) >y> g(y))

This monad is similar to the list monad in Haskell: its type is computations which produce zero or more values.

Pruning Combinator#

If we write f(x) <x< m for m >>= f, use let for "return", and require that computations in the monad produce exactly one value, the monad laws are still not quite satisfied.

  1. Left identity: f(x) <x< let(a)f(a) (true)
  2. Right identity: let(x) <x< mm (true)
  3. Associativity: g(y) <y< (f(x) <x< m)(g(y) <y< f(x)) <x< m (false)

The associativity rule fails because f may produce a value while ignoring its argument. In the left side of the equation, this would cause m to terminate, while in the right side, it would not.

For more discussion on algebraic encodings of dataflow, see http://lambda-the-ultimate.org/node/988

Add new attachment

Only authorized users are allowed to upload new attachments.
« This page (revision-1) was last changed on 06-Feb-2009 08:33 by AdrianQuark