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?