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

[Brandon S. Allbery KF8NH]

On Jan 23, 2007, at 14:48 , Robert Dockins wrote:

> Its possible, however, that I don't understand your question.  The  
> formula (p^~p)->q (AKA, proof by contradiction) is valid most  
> classical and constructive logics that I know of, so I'm not quite  
> sure what you're getting at.

I'm not expressing myself well, and I don't have the terminology or  
enough understanding of things like category theory or formal logic  
to express myself at all clearly.  :(

I am modeling _|_ in Haskell as a "failed" computation:  either a  
nonterminating computation, or an impossible operation (e.g. head  
[]).  Once you have an actualized _|_ (or a possible one, as when you  
apply seq to a computation which may be _|_), your entire computation  
is suspect.

I am modeling (p^~p)->q in logic as a "failed" production:  once you  
have produced it, your entire logical production is suspect.

It seems to me that the recent discussions about forcing strictness  
are deliberately introducing the equivalent of (p^~p)->q, and it's  
not clear to me that you can really reason about the resulting  
behavior.  The recent discussions which have seq (or alternatives)  
leading to theoretical difficulties seem to bear this out.

-- 
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