On Jan 23, 2007, at 15:50 , Neil Mitchell wrote:
> prove/compute anything you couldn't before. While removing _|_ from
> the language does make some things nicer to reason about, there
aren't
> many corners where _|_ really gets in the way that much - seq being
> one of those few corners.
But that is exactly the problem: `seq` forces _|_ to get into the
way, when it normally doesn't. So I'm not clear that trying to fit
`seq` into a formalization of Haskell's semantics is the way to go.
Agreed, that was the point I was trying to make :)
You seemed to be suggesting _|_ was "evil" (for want of a more precise
term) in its behaviour with Haskell. As you seem to say now (and I
agree), _|_ is a perfectly useful value, just seq gets in the way.
I think at this point I can finally say what I was trying to grasp at
(and missing, although I was in the right ballpark at least):
It seems to me that the notion of reasoning about Haskell programs in
terms of category theory works because category theory is in some
sense inherently lazy, whereas (for example) formal logic is
inherently strict. So the problem with reasoning about `seq` is that
it changes/breaks (depending on how you look at it) the model. Now:
either one can come up with a way to model strictness in category
theory (compare, for example, modeling I/O in pure functional
languages by means of monads), or one can accept that forcing
strictness requires reasoning via a different model. Either way,
`seq` (or strictness in general) is not really "evil". (And neither
is _|_.)
--
brandon s. allbery [linux,solaris,freebsd,perl] [EMAIL PROTECTED]
system administrator [openafs,heimdal,too many hats] [EMAIL PROTECTED]
electrical and computer engineering, carnegie mellon university KF8NH
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
