Re: Language changes: Committed choice

From: Michael Hanus <hanus_at_informatik.rwth-aachen.de>
Date: Tue, 27 Oct 1998 14:49:20 +0100

Wolfgang Lux proposed the following evaluation annotation:
> E.g. the non-deterministic merge function could be implemented as
>
> merge eval choice
> merge [] l2 = l2
> merge l1 [] = l1
> merge (e:r) l2 = e : merge r l2
> merge l1 (e:r) = e : merge l1 r

I think this is an interesting proposal because it elegantly solves
some problems which we also detected with the use of committed choice
(see Frank's answer). I agree with Herbert that there
should be only one concept for committed choice in order
to avoid confusion and keep the language primitives as simple
as possible. Recently, I also discussed with Sergio Antoy
the introduction of "matching constraints" in guards to provide
laziness in guard evaluation (as mentioned by Frank or proposed
in Goffin). The disadvantage of these matching constraints
is that they require new scoping rules for the pattern variables
which can be avoided with Wolfgang's proposal. However,
I think the description of the operational behavior is
not sufficient.

Wolfgang writes:
> Informally the semantics of a function defined with the choice
> annotation would be as follows:
> For every argument that is demanded in one the patterns, check if the
> argument is in WHNF and not an unbound variable. If any of the rules
> can be selected based on these arguments, select it. (If more than one
> rule can be selected one will be chosen randomly.)
> Otherwise, if any of the demanded arguments is not in WHNF, evaluate
> it to WHNF and then try to select a rule, again.
> If there are no demanded arguments, which are not in WHNF, but there
> are uninstantiated variables in demanded positions, suspend until (at
> least) one of these variables is instantiated.
> In any other case the evaluation fails.

Two things are unclear:
1. What is the meaning of conditions in rules? Is the commit done
   after or before condition evaluation? I think it is reasonable
   that the conditions are checked before the commit is done.
   In this case, you can also express deep guards and thus subsume
   the old committed choice.
2. What are the restrictions during the evaluation of a demanded argument
   to WHNF? Is it allowed to bind goal variables? What happens
   if this evaluation is non-deterministic?

The general idea of a committed choice is to evaluate the different
guards (or pattern matching tasks) locally and then commit to
a successful guard. Thus, I propose the following operational
behavior for a function call with evaluation annotation "choice":

Evaluate this function call as usual (with a fair evaluation of
alternatives) but
- do not bind variables occurring in this call
- ignore all alternatives if one rule matches and its guard is
  entailed (i.e., satisfiable without binding goal variables)

The first restriction is similar to the rigid annotation
but requires a rigid evaluation also for all subcalls
(as in the current "choice"). It contains Wolfgang's proposal
as a special case and answers the unclear topics.
I think with this proposal we have the same power as with
the old "choice" but avoid the special syntax and scoping
rules in the "choice".

Any comments?

Michael
Received on Di Okt 27 1998 - 18:54:00 CET