[Haskell-cafe] IO is not a monad (and seq, and in general _|_)
Robert Dockins
robdockins at fastmail.fm
Tue Jan 23 14:48:19 EST 2007
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
More information about the Haskell-Cafe
mailing list