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

[Robert Dockins]

On Jan 23, 2007, at 2:09 PM, 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,

I'm not sure you've got quite the right notion of what bottom  
"means."  There are lots of computations that are representable in  
Haskell that are equivalent to _|_.  _|_ is just a name we give to  
the class of computations that don't act right (terminate).

> 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?

You seem to be talking around the edges of the Curry-Howard  
isomorphism.  C-H basically says that there is a correspondence  
between typed lambda calculi and some logical system.  Types  
correspond to logical formulas and lambda terms correspond to  
proofs.  However, a system like Haskell's (where every type is  
inhabited) corresponds to an inconsistent logic (one where every well- 
formed statement is provable).  That just means that the logic system  
corresponding to Haskell's type system isn't a very useful one.   
However, we don't reason _about_ Haskell using that logic, so its not  
really a problem.

Its possible, however, that I don't understand your question.  The  
formula (p^~p)->q (AKA, proof by contradiction) is valid most  
classical and constructive logics that I know of, so I'm not quite  
sure what you're getting at.



Rob Dockins

Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
           -- TMBG