> > Oh, but _|_ is a member of the type Boolean.
> > _|_ is a member of all types.
> >
> > For instance, I can write the following:
>
> Someone else said this as well.
> Every login textbook I have seen says that to be a boolean is
> to be either True or False, not True, False, or I_dunno.
> Don't mistake features of the simulation for features of reality.
> As an implementation matter, Haskell allows you to pass _|_ to a
> function that takes only boolean arguments. That does not mean
> _|_ is a boolean.
> It does mean that Haskell's model for booleans is less than perfect.
There seems to be serious confusion here!
True and False are the only "fully determined" members of Bool. But,
even in imperative languages, it is possible for a boolean-typed
expression to diverge, or possibly cause an error -- neither of these is
True or False. So the question to every language designer that permits
this is: How do you handle this situation? If the answer is given in
terms of denotational semantics, then the notion of _|_ invariably
creeps in, or possibly even more complex domains with error elements,
etc. This is not something unique to Haskell.
Haskell's particular solution, of course, is that both divergence and
errors are modelled in the same way: as _|_. More precisely, Bool is
modelled as a a flat domain with incomparable values True and False, and
least (bottom) element _|_. The bottom element in each data type in
Haskell is UNIQUE, however: _|_ in Bool is different from _|_ in Int,
etc, and they are usually distinguished by subscripting, as in
\perp_{Bool} in LaTeX terms. On the other hand, the completely
polymorphic type "a" can be used to represent all of these bottom
values, as it will take on the value of the appropriate version of _|_
in a given context. That _|_ is the ONLY inhabitant of this completely
polymorphic type is really a result of parametricity.
Although identifying errors with non-termination is somewhat
over-simplistic, it generally simplifies equational reasoning, where we
like to think in terms of "values", even though non-termination and an
error are not really "values".
So as pointed out by others, a && b is not the same as b && a, simply
because && is strict in its first argument (but not in its second).
That is, _|_ && e is always _|_, whereas e && _|_ is not (necessarily)
_|_. But note that this is also true in most imperative languages, even
when e has no side effects! Operationally speaking, both Haskell and
other langauges evaluate the first argument, and then ONLY IF THAT VALUE
IS TRUE is the second argument evaluated. So of course && is not
commutative.
I hope this helps,
-Paul
