Re: Local pattern declarations in Curry
> I understand it from an operational point of view, but could
> you refer to some theory justifying this view?
> Maybe the UC Madrid group can help?
I think, we have (at least) four options:
1) adapt the theory developed in the ESOP'96 paper to
the special treatment of nullary functions (i.e. that the
same value is shared between all occurrences). Maybe,
the UCM group could comment on this possibility!?
2) transform out nullary functions (such that the
existing theory can used)
3) adopt Michael's original proposal
(no sharing of values for locally defined nullary functions)
4) Michael's last proposal
locally defined nullary functions are handled like variables
(i.e. their values are shared); locally defined recursive
nullary functions are forbidden
I will comment below on possibilities 2) and 4). Moreover, I would
like to remember that 3) leads to some surprising behaviour, e.g. in
psort xs | sorted ys = ys where ys = permut xs
Honestly, who was able to spot immediately that this
definition does not work as expected?!
I would also like to note that something like this
is not artificial (like the many other examples, we were
discussing) but usual programming practice.
to 2):
The whole program could be understood as syntactic sugar
for
dummy_lhs = goal where definitions
Thus, the "top level" definitions would be handled just
like local definitions as pointed out in my last email.
> coin = 0
> coin = 1
> ...
> f xs = ...coin...
> g ys = ...coin...
> ...
For the example, this means:
(assuming the goal is f Xs)
dummy_lhs = h xs
h xs = f1 xs
h xs = f2 xs
f1 xs = ... coin1 ...
f2 xs= ... coin2...
g1 xs= ... coin1...
g2 xs= ... coin2 ...
coin1 = 0
coin2 = 1
Note that this just serves to transform the program to the
kernel language in order to explain its meaning based on the
existing theory (i.e. mainly the ESOP'96 paper). It does
NOT imply that Curry programs have to implemented
like this. A possible implementation could preserve
the nesting and avoid the code explosion.
to 4) this proposal avoids the surprising behaviour in the
permutation sort example, but restricts the language.
Unfortunately, it also destroys the compatibility with
Haskell. In order to recover it, one could allow
deterministic locally defined recursive
nullary functions (and handle them by lambda
lifting). Thus, only non-deterministic locally defined
recursive nullary functions remain excluded.
This seems to be acceptable (the length of the name
indicates, how often they are needed), especially since the user
can avoid them by applying the proposed
transformation by hand.
Best regards,
Herbert
Received on Fr Nov 13 1998 - 12:11:00 CET
This archive was generated by hypermail 2.3.0
: Do Jun 20 2024 - 07:15:06 CEST