Re: Local pattern declarations in Curry

From: Herbert Kuchen <kuchen_at_uni-muenster.de>
Date: Fri, 13 Nov 1998 12:03:45 +0000

> 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