[Haskell-cafe] Re: Monad definition question

[Ilya Tsindlekht]

On Sat, May 05, 2007 at 12:09:03AM -0700, oleg at 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.
>