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? _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
