On Sat, May 05, 2007 at 12:09:03AM -0700, oleg@pobox.com wrote:

Ilya Tsindlekht wrote:

...

Does the definition of monad silently assume that if f and f' are equal in the sense that they return the same value for any argument o correct type then m >>= f = m >>= f'

Of course NOT! Here's an example, in a State monad

f x = put True f' x = put False Clearly, _by the definition above_, f and f' are the same -- for any argument of correct type, they return the same value, namely,

They aren't - they return different values of type State Bool ()

(). However, if we perform the observation

execState (return 'a' >>= f) True execState (return 'a' >>= f') True

we quite clearly see the difference. Of course - because f 'a' and f' 'a' are different values. (return 'a' >>= f is by laws of monad the same as f 'a')

Robin Green wrote:

...

How could it be otherwise? How are you going to distinguish between f and f' if they are indistinguishable functions, in Haskell?

Because f and f' are NOT referentially transparent functions. They are NOT pure functions, their application may have _an effect_. And They ARE pure functions (just as all Haskell functions) They return values of monad type. comparing effectful computations is quite difficult. It's possible: I believe (bi)simulation is the best approach; there are other approaches.

It may be useful to relate to imperative programming: m1 >>= (\x -> m2) is let x = m1 in m2 The analogy is not always straight-forward - try the list monad. Indeed, monadic 'bind' is *exactly* equivalent to 'let' of impure eager languages such as ML. The first monadic law return x >>= f === f x is trivial because in eager languages, any value (which is an effectful-free computation) is by default injected into the world of possibly effectful expressions: Any value is an expression. The second law m >>= (\x -> return x) === m becomes let x = e in x === e and the third law (m1 >>= (\x -> m2)) >>= (\y -> m3) === m1 >>= (\x -> m2 >>= \y -> m3) provided x is not free in m3 becomes let y = (let x = m1 in m2) in m3 === let x = m1 in let y = m2 in m3

So, `bind' is `let' and monadic programming is equivalent to programming in the A-normal form. That is indeed all there is to monads.

Here's the paragraph from the first page of Filinski's `Representing Monads' (POPL94)

"It is somewhat remarkable that monads have had no comparable impact on ``impure'' functional programming. Perhaps the main reason is that -- as clearly observed by Moggi, but perhaps not as widely appreciated in the ``purely functional'' community -- the monadic framework is already built into the semantic core of eager functional languages with effects, and need not be expressed explicitly. ``Impure'' constructs, both linguistic (e.g., updatable state, exceptions, or first-class continuations) and external to the language (I/O, OS interface, etc.), all obey a monadic discipline. The only aspect that would seem missing is the ability for programmers to use their own, application-specific monadic abstractions -- such as nondeterminism or parsers [31] -- with the same ease and naturality as built-in effects."

Filinski then showed that the latter seemingly missing aspect indeed only appears to be missing. Would this require some kind of macros doing extensive pre-processing of the code?

It is important to understand that once we come to monads, we lost referential transparency. Monadic code is more difficult to reason about -- as any imperative code. One often sees the slogan that Haskell is the best imperative language. And with monad, it is. One often forgets that 'best' here has the down-side. Haskell amplifies both advantages _and_ disadvantages of imperative programming. At least imperative programmers don't have to think about placing seq at the right place to make sure a file is read from before it is closed, and don't have to think about unsafeInterleaveIO. It seems the latter has become so indispensable that it is recommended to Haskell novices without a second thought. One may wonder if functional programming still matters.