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.