On Jan 23, 2007, at 14:58 , Seth Gordon wrote:
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.
That's not quite what I was trying to say. (p^~p)->q is equivalent to _|_ in the sense that once you derive/compute (respectively) it, the "world" in which it exists breaks. (I don't think formal logic can have a Haskell-like _|_, but deriving (p^~p)->q is close to it in effect.) -- brandon s. allbery [linux,solaris,freebsd,perl] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH