> Haskell's (&&) only models the logical AND when it is passed booleans.
> To say that _|_ is a Haskell Boolean, is to create another concept
> domain (Haskell Boolean), which shares many properties with Logic
> Boolean but is not identical with it.
Right, but it is important to realize that when reasoning about programs
in most languages, the "logical" Boolean domain is not enough, since
most languages permit errors and non-termination; thus a richer domain
is needed.
> Understood in this manner, I don't think Parallel Haskell
> implementations need to make any promises about the sanity of the
> behvaior of functions when passed _|_.
I believe they do, if they claim to be "correct" implementations of a
given language. For example, if in Haskell _|_ && e is defined to be
_|_, then ANY correct implementation is obliged to observe this, whether
parallel or not (and thus enters discussions of "serial" vs
"sequential", etc.).
If a parallel Haskell implementation chooses to add a parallel &&, then
it could do so via a library using some other name, perhaps &&&.
Parallel &&& is defined such that both False &&& _|_ and _|_ &&& False
are both False; i.e. &&& is commutative. This can't be done with a
sequential implementation (at least not without interleaving to simulate
parallel execution).
> As a practical matter, it would be nice if
> program success/failure was consistent accross Haskell
> implementations, but this does not require that functions behave
> in any particularly sane manner when passed _|_, only that they
> behave consistently.
I'm not sure what you mean by "sane" vs "consistent".
> PS Charity claims to eliminate _|_. I don't know enough about
> category theory and programming language design to know the
> costs of doing so.
I have no idea what Charity is, but if this is indeed the case then, at
least for Booleans, all expressions must be strongly normalizing, i.e.
will always terminate with value True or False. Usually languages such
as these sacrifice expressivity (for example, no general recursion!),
such as languages based on constructive type theory. (Either that or
they have solved the halting problem :-)
-Paul
