On Mon 27 Sep, Bjorn Lisper wrote:
> Adrian Hey <[EMAIL PROTECTED]>:
> >This seems completely contrary to normal equational reasoning (which is
> >one thing functional languages are supposed to support), where we aren't
> >so constrained.
>
> No. Equational reasoning simply means that we use equations which are valid
> to transform expressions. When used for program transformations, the set of
> valid equations is determined by the semantics of the language. This set of
> equations will change depending on whether the language is strict or
> nonstrict. 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.
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.
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.
> Nonstrict languages actually have the property that function definitions can
> be seen as equations.
Almost, but not quite, as Fergus Henderson noted.
> I would say this is what makes the language
> referentially transparent! This means that a function call can always be
> symbolically unfolded without altering the semantics. Strict languages do
> not have this property in general. So in this sense nonstrict languages are
> more amenable to equational reasoning!
> Note that if we want the transformations to preserve the semantics of the
> language w.r.t. termination we will have to deal with bottom in equations
> also in strict languages, since also strict languages contain certain
> operations with nonstrict semantics (e.g., conditionals). Of course, we can
> consider a coarser semantics without the bottom, where we do not distinguish
> functions w.r.t. termination properties, and then have a different set of
> equalities: a good example is x - x = 0 which is valid if bottom is
> discarded but not valid if it is included. (I believe it may be this kind of
> discrepancy which has lead you to think that nonstrict languages do not
> permit equational reasoning.)
I didn't say they did not permit equational reasoning. I only said that
they complicate it (as in your example above), by forcing us to consider
_|_ as a value. The result seems to be that many intuative and useful
transformations are invalidated.
> >So is it unfair to say that as soon as issues like strict vs. non-strict
> >semantics become an important, the language is no longer purely functional?
>
> It is not only unfair, it is wrong.
Well, I suppose it depends what you call purely functional. I would
say that a language which derives it's semantics from specific (non general)
assumptions about the nature of the underlying computational machinery
is less than ideal.
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.
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?
Regards
--
Adrian Hey
