[Haskell-cafe] IO is not a monad (and seq, and in general _|_)
Brandon S. Allbery KF8NH
allbery at ece.cmu.edu
Tue Jan 23 16:33:07 EST 2007
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] allbery at kf8nh.com
system administrator [openafs,heimdal,too many hats] allbery at ece.cmu.edu
electrical and computer engineering, carnegie mellon university KF8NH
More information about the Haskell-Cafe
mailing list