[Haskell-cafe] Re: Monad definition question
oleg at pobox.com
oleg at pobox.com
Sat May 5 03:09:03 EDT 2007
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,
(). However, if we perform the observation
execState (return 'a' >>= f) True
execState (return 'a' >>= f') True
we quite clearly see the difference.
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
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
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.
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.
More information about the Haskell-Cafe
mailing list