>On Mon 27 Sep, Bjorn Lisper (i.e., me) wrote:
....
>> For instance, a logical or which is strict in both arguments will
>> be commutative and associative, while a nonstrict or with a left-to-right
>> evaluation order of its arguments will be non-commutative but still
>> associative.
>
Adrian Hey:
>But should we let such operational issues muddy the waters?
>
>Is a function..
>
> 1- A mapping between input values and output values (which don't include
> _|_). I imagine this is what mathematicians would call a function.
>
>or..
>
> 2- A method of computation. For all its abstraction, as far as Haskell
> is concerned this has to be the correct way to view a function. This
> is what makes Haskell a _programming_ language, rather than a tool
> for reasoning about the properties of functions.
In my example, it's both. On one hand, we can give a purely equational
specification of the nonstrict or I sketched above (I just give the
nonstrict part):
true or bot = true
false or bot = bot
bot or x = bot, for all x
On the other hand, it is well known that one particular reduction strategy
that implements this semantics faithfully is the classical left-to-right
strategy.
>So, I guess the answer is.. Yes, we do need to let such operational
>issues muddy the waters. What worries me here is that there might be
>some unjustifiable assumptions about the nature of the machine which is
>performing those operations. In particular by talking about things
>like 'reduction order' and 'order of pattern matching' aren't we
>assuming a sequential machine. If so, should such considerations be
>allowed to 'pollute' the semantics of a general purpose high level
>programming language.
We are not assuming a sequential machine. The equational semantics of "or"
above does for instance allow that we speculatively fork off a thread
evaluating the second argument before we know the value of the first
argument, if we just delay the return of the answer until the first argument
is fully evaluated. On the other hand, one must keep some operational
semantics in mind when specifying a more abstract semantics, so one does not
end up with a language which is very expensive or impossible to implement on
the machines at hand.
>> Nonstrict languages actually have the property that function definitions can
>> be seen as equations.
>
>Almost, but not quite, as Fergus Henderson noted.
Well, as Fergus pointed out, syntactic sugar like definitions by patterns
may have to be removed first.
....
>What started me thinking about this is the 'World as Value' thread on the
>Clean discussion list, where I tried (unsuccessfully I suspect) to make the
>case for using a concurrent non-deterministic machine as the basic model
>for I/O.
>
>Then I started thinking about how one would compile function definitions
>into 'computational actions' on such a machine (a Haskell compiler does
>this for sequential machines) and realised that this would give that
>language subtly different semantics wrt the way _|_ was treated. I don't
>know what the proper name for such semantics is, so I'll call it
>'concurrent non-strict' semantics as distinct from 'sequential non-strict'
>semantics.
Do you think about such semantics as the "parallel or", which has its
strictness properties defined by:
false or bot = bot or false = bot
true or bot = bot or true = true
?
>I think concurrent non-strict semantics restores many (perhaps all?)
>useful transformations. An obvious example being it restores
>transformations like..
> a && b = b && a
>
>Does this make sense?
Yes, it makes a lot of sense. The parallel or above is a classical example
of a function for which there exists no semantically correct sequential
evaluation order of its arguments (i.e., an evaluation order where an
argument is evaluated in full before the evaluation of the next argument
starts). Therefore, it has usually been discarded as infeasible to implement
since the in the worst-case scenario its evaluation may require that you
spawn off an exponential number of concurrent threads (imagine a function
calling the parallel or recursively on both sides).
Bj�rn Lisper
