Re: Haskell and Parallelism (was: What is a functional language?)

[S. Alexander Jacobson]

My simple point is that claims about the correctness or incorrectness of
the behavior of a function are incoherent outside the function's domain;
that, as an language implementation matter, it is handy to make _|_ a
member of all types is irrelevant.  

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.

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 _|_.  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.

-Alex-

PS Charity claims to eliminate _|_.  I don't know enough about category
theory and programming language design to know the costs of doing so.

___________________________________________________________________
S. Alexander Jacobson                   Shop.Com
1-212-697-0184 voice                    The Easiest Way To Shop



On Tue, 28 Sep 1999, Paul Hudak wrote:

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