[Haskell-cafe] Monad definition question

[Ilya Tsindlekht]

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'

More specifically, the definition says x >>= return = x. How does one
justify from this that x >>= (return . id) = x?

Are values of type a -> b in general assumed to be maps from the set of
values of type a into the set ov values of type b? (What bothers me is
that the problem whether two lambda-expressions define the same map is
clearly undecidable.)

More generally, is some kind of logic without equality more appropriate
for formalisation of Haskell then the usual kind(s) of logic with
equality?
_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Robin Green]

On Fri, 04 May 2007 14:42:53 +0300
Ilya Tsindlekht <eily...@013.net> 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'

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

> More specifically, the definition says x >>= return = x. How does one
> justify from this that x >>= (return . id) = x?
>
> Are values of type a -> b in general assumed to be maps from the set
> of values of type a into the set ov values of type b?

Yes - if _|_ is considered to be a value.

> (What bothers
> me is that the problem whether two lambda-expressions define the same
> map is clearly undecidable.)

Yes. But this is a fundamental mathematical issue which isn't at all
specific to Haskell, of course. It suggests using some sort of
intensional type theory, so that you have to explicitly prove lambda
expressions to be equal.

> More generally, is some kind of logic without equality more
> appropriate for formalisation of Haskell then the usual kind(s) of
> logic with equality?

I suggest you look into Observational Type Theory.
--
Robin

[ol...@pobox.com]

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.

[Ilya Tsindlekht]

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

Would this require some kind of macros doing extensive pre-processing
of the code?

[ol...@pobox.com]

Ilya Tsindlekht wrote

> > 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.

This equivalence holds even for the List Monad. Here is an example of
non-determinism:

http://caml.inria.fr/pub/ml-archives/caml-list/2007/02/1d4df471019050b89e20a002303a8498.en.html

and here's an excerpt from that message, showing lets (aka bind):

let numbers = List.map (fun n -> (fun () -> n)) [1;2;3;4;5];;
let pyth () =
let (v1,v2,v3) =
let i = amb numbers in
let j = amb numbers in
let k = amb numbers in
if i*i + j*j = k*k then (i,j,k) else failwith "too bad"
in Printf.printf "got the result (%d,%d,%d)\n" v1 v2 v3;;

Here, 'amb' is like 'msum' and any error is mzero. If we replace 'let'
with 'do', and '=' with '<-' in some places, it looks almost like
Haskell. Although the scheduler (the `run' function of the `monad')
described in the message accumulates all possible worlds, it returns
as soon as one `thread' made it successfully to the end. It is
trivial to get the scheduler to run the remaining `treads' searching
for more answers (by threads I certainly don't mean OS threads). The
user code above stays as it is.

The implementation of amb has been extended to annotate choices (and
so possible worlds) with probabilities, which propagate in due
course. The result not merely lists the answers but also their
computed probabilities.

> > 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?

Hopefully the code above showed that no macros and no preprocessing
required. In that code, addition, multiplication, if-then-else and all
other OCaml operations remain as they have always been, with no
modifications or redefinitions whatsoever. Delimited continuations
suffice for everything, as Filinski proved in his paper.