[Haskell-cafe] IO is not a monad (and seq, and in general _|_)
sethg at ropine.com
Tue Jan 23 14:58:34 EST 2007
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:
> 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
(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?
More information about the Haskell-Cafe