Re: Curry mailing list (welcome)

From: Michael Hanus <hanus_at_medoc.informatik.rwth-aachen.de>
Date: Mon, 16 Dec 1996 15:50:58 +0100

Dear Sergio,

Thanks for your comments on our proposal.

Concerning your comment about the simultaneous definition
of types, evals, and equations, I would like to separate them
since then we need no special rule or syntax if the type and/or
evaluation annotation is omitted. I expect that the evals
are omitted in most cases (similarly to Prolog where the
standard computation rule is also sufficient in most cases).
On the other hand, the separated pieces do not contain much redundancy
(apart from the function name) in contrast to your Algol example.
Furthermore, as Herbert already remarked, it is difficult to combine
the annotations with the single equations. However, I am open to
new suggestions. Currently, I can imagine to omit only
the repeated mentioning of the function name, e.g., to define
append (Section A.1) by

append: List t -> List t -> List t eval 1:flex
       [] ys := ys
       [x|xs] ys := [x|append xs ys]

However, this is a little bit against the "traditional" notation
of functional and logic languages.

> ------------------------------------------------------------------
>
> The restriction on the variables in the right hand side of a
> (conditional) equation makes it impossible to define a function f
> such as
>
> f x := y if y = x
>
> which is certainly well-behaved and allowed in many functional
> languages. There is some work by Middeldorp and others that
> relaxes Curry's restrictions and yet guarantees confluence (the
> function is well defined) in situations such as the above example.
> We implemented it in our functional extension of Goedel and it was
> not very hard. So my question is: "Has this issue been studied
> enough or should we study more the issue of the extra variables in
> the right hand side of conditional equations?"

This is an interesting point. In this proposal, I just wrote
the restrictions of Babel ensuring confluence, but I fully agree
that Curry should also provide a more general view. For instance,
it may be interesting to write functions with extra-variables
in the right-hand side where the confluence is not obvious, like in

last xs = x if append _ [x] = xs

(This example runs perfectly in our current implementation.)

This is more than the "where" clauses in current functional languages,
and such applications have not been studied enough. On the other hand,
as far as I know, the work by Middeldorp, Suzuki and Ida shows
that the common "where" clauses, where the extra-variables are
instantiated by pattern matching, ensures level-confluence and
completeness of narrowing. Since such uses of extra-variables
provides a direction in the computation, maybe it is better
to express it better by where-clauses than arbitrary conditions,
i.e., your example could be expressed by

f x := y
       where y := x

I would be happy if you could extend the current proposal to
extra-variables in right-hand sides of equations.

Best regards,

Michael
Received on Mo Dez 16 1996 - 15:53:14 CET