Paul Hudak wrote:
Hi Claus --
I think that you're asking for a semantics of the entire OS, i.e. the
entire outside world, and for that I agree that something other than
equational reasoning is needed to reason about it. However, I would
argue that that is outside the mandate of a book on Haskell. But
maybe that's the point -- i.e. others feel otherwise.
My main point it that if we're reasoning about a single Haskell
program (with no impure features), then the entire world, with all its
non-determinism internal to it, can be modelled as a black box --
i.e. a function -- that interacts with the single Haskell program in a
completely sequential, deterministic manner. And for that, equational
reasoning is perfectly adequate.
I think the problem is that to understand something you need a lot more than
just the capability to reason about it.
For example, given laws such as:
x * (y + z) == (x * y) + (x * z)
x + (y + z) = (x + y) + z
I can reason that
x * (y + (z + w)) = (x * y + x * z) + x * w
But this does *not* mean that therefore I *understand* it. I think
understanding is a much deeper process. I have to grapple with the
underlying shape, the gesture, the motion of the symbolic transformation and
really *feel* the lawfulness of it as a profound inner life experience.
So to get back to the question of understanding monads, yes I can reason
about them equationally using pure functions but to understand Haskell I
need to understand how it is situated in my own human experience and my
human experience seems to me to be more than just a deterministic sequential
function of Unique -> Time -> SenseInput.
Regards, Brian.
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
