
Duncan Coutts
On Sun, 2006-07-30 at 10:56 +0100, Jón Fairbairn wrote:
"David House"
writes: 1) f is strict iff f _|_ = _|_. 2) f is strict iff it forces evaluation of its arguments.
In (2), you have to be evaluating f on an argument before f can force the argument. If you evaluate id x, you necessarily evaluate x. I don't think (2) is a very good definition, since I don't know what "forces" means here.
Surely it just means evaluate to weak head normal form?
Means [what] evaluate[s] to whnf? id doesn't do any evaluating, in fact functions in general don't do any evaluating.
Definition 2) relies on following a certain evaluation strategy: that operationally, functions always return results in weak head normal form. GHC follows this strategy. It's possibly to imagine returning thunks and then getting the caller to force the evaluation to WHNF.
Which is pretty much my point. Use a definition of "strict" that doesn't depend on anything but denotations (or Böhm trees). -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk