!! Monad Laws

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

# Left identity: (return ''a'') >>= ''f''  ≡  ''f a''
# Right identity: ''m'' >>= return  ≡  ''m''
# Associativity: (''m'' >>= ''f'') >>= ''g''  ≡  ''m'' >>= (λ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.

# Left identity: {{let(a) >x> f(x)}} ≡ {{f(a)}}
# Right identity: {{m >x> let(x)}} ≡ {{m}}
# 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.

# Left identity: {{f(x) <x< let(a)}} ≡ {{f(a)}} (true)
# Right identity: {{let(x) <x< m}} ≡ {{m}} (true)
# 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