Dear "curritos" (workers, in spanish slang):
Most of the people in the Declarative Programming Group in Madrid
(Univ. Complutense) consider the Curry iniciative as a very interesting
and promising one, and would like our group to participate
in it. After a meeting, we decided to create a small local
Curry committee (Ana Gil, Teresa Hortala, Mario Rodriguez,
Eva Ullan and myself) and to use, as much as possible,
a unique voice (mine!) for translating our opininionsto the Curry
discussion.
First of all, we apologize if we incorporate a bit late to the
discussion.
Our first block of technical considerations is the following:
1. With respect to the question of including 'let' and 'where'
constructions in a Haskell style, which has been discussed in some
messages, we are definitely in favour of that inclusion. Although
'let' and 'where' can be lifted (and this of course can be
taken into account when discussing many aspects of the language)
they prove to be very useful in practice.
2. With respect to the question of allowing extra variables in
right-hand sides, our opinion is quite radical: we strongly
advocate to adopt non-deterministic functions as the fundamental
notion underlying the language, instead of the 'classical'
of deterministic function. The problem of variables in rhs
vanishes, since they can be used freely. Some arguments
supporting this (admitedly controversial) point of view follow:
- As it has already been implicitely pointed out by Michael
> (but the compiler accepts also the more general cases
> which cause no implementation problems in a functional
> logic language)
non-deterministic functions are implemented for free in most
functional logic systems, even if they are not meant for this.
- Computing with deterministic functions presents some adventages
(e.g., dynamic cut), but these benefits are NOT lost when you
have a system supporting non-deterministic functions. The following
statement tries to make it clear: whichever decidable conditions you
establish ensuring that your program is legal, that is,
it really defines 'classical' (i.e. deterministic) functions,
these conditions can be re-used, in a non-deterministic setting,
for detecting that some (probably most) of the functions in
a program are deterministic, hence allowing the use of
optimizations for such cases.
- To provide mathematical (model theoretic, proof theoretic,
fixpoint) semantics to programs and computations with
nondeterministic functions is possible.
We have some works along this line (see, f.i.,
"A Rewriting Logic for Declarative Programming" (ESOP'96)
which can be found in
http://mozart.mat.ucm.es )
- Non-deterministic functions are interesting by themselves
as a programming language construct. This is specially true
when functions are lazy (the case of Curry). For instance,
you can lazily non-deterministically generate objects (even
infinite) which are then checked for a desired property.
That is, you can write "efficient" generate-and-test programs,
in contrast with the case of similar logic programs (which
are typically inneficient) or the case of similar functional programs
(which are efficient, but at the cost of constructing some kind
of "list-of-all-objects").
As an example, consider the following program for "permutation
sort" (Sergio has a similar example in one of his papers):
% // is the nondeterministic function by excellence
x // y := x
x // y := y
% Nondeterministic insertion in a list
insert x [] := [x]
insert x [y|ys] := [x,y|ys]
//
[y|insert x ys]
% Non-deterministic generation of permutations
permut [] := []
permut [x|xs] := insert x (permut xs)
% In the following definition, 'ys' (i.e. 'permut xs')
% is lazily generated, as much as the filter 'sorted' demands it.
% The filter may reject 'ys' without fully constructing it.
sort xs := ys if sorted ys
where ys := permut xs
sorted [] := true
sorted [x] := true
sorted [x,y|ys] = sorted [y|ys] if x <= y
3. The question of equality (p. 4-5 in the Curry report) should
be clarified. Some comments and suggestions about that:
* We accept the convenience of considering two kinds of equality,
otherwise disequality constraints should be used and this
complicates the language in the overall.
* In a first moment, in p.4, some rules are given for strict equality,
which are meant to correspond to the equality used in functional
languages. This is not true: equality in FL is two-valued (may return
'true' or 'false'), and this is not the case for the mentioned set
of rules. The set of rules appropriate for equality in FL is
in fact the rules given for == in p.5.
* Contrary to the case of ==, the equality =, as described in p. 5,
can only return the value 'true'. Therefore, it is not correct to speak
about
"two kinds of equalities which have identical meaning on
ground expressions". In fact, = could be 'defined' by means of
the set of rules in p.4 (although the implementation would
not follow the 'normal' mechanism of evaluation, because the generation
of infinite ground solutions is replaced by unification).
* A question: do you think that the report should fix the evaluation
strategy for = and ==? We think not. For instance, one implementation
could, for simplicity, evaluate e=e' by reducing e and e' to normal
form before performing unification (this is the mechanism suggested
in p. 5). But other implementations could try more sophisticated
ways for performing unification incrementally. This done so,
e.g, in our implementations (TOY, BabLog).
That's all for the moment for the technical stuff. In the organizative
level of the Curry iniciative, we think that it would be convenient:
1. To identify the different institutions o groups which want
to be involved in the Curry initiative.
2. To have a representant of each group.
3. To start thinking about possible mechanisms for taking decisions.
What is your opinion about that?
Best regards,
Paco Lopez,
--
Francisco J. Lopez-Fraguas
Dep. Informatica y Automatica
Fac. Matematicas Av. Complutense s/n
Universidad Complutense de Madrid
28040 Madrid
SPAIN
Phone: +34 1 3944429
Fax: +34 1 3944607
email: fraguas_at_dia.ucm.es
Received on Do Jan 23 1997 - 18:38:18 CET