[Haskell-cafe] IO is not a monad (and seq, and in general _|_)

[Brandon S. Allbery KF8NH]

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