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

[Seth Gordon]

Brandon S. Allbery KF8NH wrote:
> Can someone explain to me, given that (a) I'm not particularly expert 
> at maths, (b) I'm not particularly expert at Haskell, and (c) I'm a  bit
> fuzzybrained of late:

Me too...

> Given that _|_ represents in some sense any computation not 
> representable in and/or not consistent with Haskell, why/how is 
> reasoning about Haskell program behavior in the presence of _|_ *not* 
> like reasoning about logic behavior in the presence of (p^~p)->q?

The only catch I see to that POV is that the way `seq` is defined,
"undefined `seq` 42" *must* return an error.  If this were analogous to
"(p^~p)->q", then "undefined `seq` 42" would be allowed to return any
value whatsoever.

(Imagine an "unsafeSeq" operator, such that "undefined `unsafeSeq` 42"
could *either* raise an exception or return 42, and implementations
would be free to replace "a `unsafeSeq` b" with "b" when optimizing.
Would this be useful?)

Can we treat "a `seq` b" as a sort of pragma and not a "real" function?
 Does Haskell semantics become tractable again if we treat Haskell
excluding "seq" (and excluding exceptions? and excluding threads?) as a
category, and the exceptions as operating on some kind of meta-level?