Editing Monad laws (section)

== The monad laws in practice ==

If we re-write the laws using Haskell's <code>do</code>-notation:

{|
|-
| ''Left identity:''
| <haskell>
do
  x′ <- return x
  f x′
</haskell>
| ≡
| <haskell>
do
  f x
</haskell>
|-
| ''Right identity:''
| <haskell>
do
  x <- m
  return x
</haskell>
| ≡
| <haskell>
do
  m
</haskell>
|-
| ''Associativity:''
| <haskell>
do
  y <- do
    x <- m
    f x
  g y
</haskell>
| ≡
| <haskell>
do
  x <- m
  do
    y <- f x
    g y
</haskell>
| ≡
| <haskell>
do
  x <- m
  y <- f x
  g y
</haskell>
|}

we can see that the laws represent plain, ordinary common-sense transformations of imperative programs.

=== But why should monadic types satisfy these laws? ===
----
When we see a program written in a form on the left-hand side, we expect it to do the same thing as the corresponding right-hand side; and vice versa.  And in practice, people do write like the lengthier left-hand side once in a while.

* First example: beginners tend to write

:<haskell>
skip_and_get = do
  unused <- getLine
  line <- getLine
  return line
</haskell>

:and it would really throw off both beginners and veterans if that did not act like (by ''right identity''):

:<haskell>
skip_and_get = do
  unused <- getLine
  getLine
</haskell>

* Second example: Next, you go ahead and use <code>skip_and_get</code>:

:<haskell>
main = do
  answer <- skip_and_get
  putStrLn answer
</haskell>

:The most popular way of comprehending this program is by ''inlining'' (whether the compiler does or not is an orthogonal issue):

:<haskell>
main = do
  answer <- do
    unused <- getLine
    getLine
  putStrLn answer
</haskell>

:and applying associativity so you can pretend it is:

:<haskell>
main = do
  unused <- getLine
  answer <- getLine
  putStrLn answer
</haskell>

The associativity law is amazingly pervasive: you have always assumed it, and you have never noticed it. 

The associativity of a ''binary'' operator allows for any number of operands to be combined by applying the binary operator with any arbitrary grouping to get the same well-defined result, just like the result of summing up a list of numbers is fully defined by the binary <code>(+)</code> operator no matter which parenthesization is used (yes, just like in folding a list of any type of monoidal values). 

Whether compilers make use of them or not, you still want the laws for your own sake, just so you can avoid pulling your hair out over counter-intuitive program behaviour, which depends (in brittle fashion!) on e.g. how many redundant <code>return</code>s you insert or how you nest your <code>do</code>-blocks...

[[Category:Standard_classes]]
[[Category:Monad]]