[Haskell-cafe] IO is not a monad (and seq, and in general _|_)
Brandon S. Allbery KF8NH
allbery at ece.cmu.edu
Tue Jan 23 15:03:34 EST 2007
On Jan 23, 2007, at 14:48 , Robert Dockins wrote:
> 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.
I'm not expressing myself well, and I don't have the terminology or
enough understanding of things like category theory or formal logic
to express myself at all clearly. :(
I am modeling _|_ in Haskell as a "failed" computation: either a
nonterminating computation, or an impossible operation (e.g. head
[]). Once you have an actualized _|_ (or a possible one, as when you
apply seq to a computation which may be _|_), your entire computation
is suspect.
I am modeling (p^~p)->q in logic as a "failed" production: once you
have produced it, your entire logical production is suspect.
It seems to me that the recent discussions about forcing strictness
are deliberately introducing the equivalent of (p^~p)->q, and it's
not clear to me that you can really reason about the resulting
behavior. The recent discussions which have seq (or alternatives)
leading to theoretical difficulties seem to bear this out.
--
brandon s. allbery [linux,solaris,freebsd,perl] allbery at kf8nh.com
system administrator [openafs,heimdal,too many hats] allbery at ece.cmu.edu
electrical and computer engineering, carnegie mellon university KF8NH
More information about the Haskell-Cafe
mailing list