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

[Greg Buchholz]

Brandon S. Allbery KF8NH wrote:
> 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.)

Here's a couple of papers you might like...

"Fast and Loose Reasoning is Morally Correct"
http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/fast+loose.pdf

"Precise Reasoning About Non-strict Functional Programs
  How to Chase Bottoms, and How to Ignore Them"
http://www.cs.chalmers.se/~nad/publications/danielsson-lic.pdf

"Total Functional Programming"
http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf

Greg Buchholz