[Haskell-cafe] The values of infinite lists
paul.hudak at yale.edu
Wed May 24 11:41:25 EDT 2006
Brian Hulley wrote:
> Paul Hudak wrote:
>> 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 ...
I agree with all of this. But then you say:
> and my
> human experience seems to me to be more than just a deterministic
> sequential function of Unique -> Time -> SenseInput.
This seems like a value judgement. Someone else might very much like
the functional model of things, and might not like some other model.
And one might argue that if the functional view is the same as the view
that one is using to reason about the rest of the program, then that is
a Good Thing. So I'm not saying that there aren't other approaches
(denotational semantics, operational semantics, process calculi, etc.)
but they might each have the problem of "understanding how it is
situated in my own human experience".
More information about the Haskell-Cafe