Committed Choice (Was: Summary of changes)

From: Wolfgang Lux <>
Date: Thu, 02 Dec 2004 14:20:35 +0100

Michael Hanus wrote:

> 5. As a replacement of "eval choice", the prelude defines
> a new primitive function
> commit :: [(Success,a)] -> a
> that takes a list of constraint/expression pairs and returns
> one of the expressions whose constraint is satisfied
> (without binding variables that are not local to the
> constraint/expression pair).

There is a subtle problem here. Which variables are considered
local and may be bound during the evaluation of the constraint
expression? I guess you mean that only variables which are
introduced during the evaluation of the constraints may be bound
(at least this is the only reasonable definition of local I can
imagine). However, this means that

   coin 0 = success
   coin 1 = success

   oneCoin = commit [let x free in (coin x,x)]

will not work. At least it would not work with MCC because oneCoin
is transformed into let x free in commit [(coin x,x)], for which
the variable shared between the constraint and the expression is
obviously defined before commit is evaluated. Note that the
normalization in [AH+02] will transform oneCoin in a similar way.
One might use an auxiliary function in order to prevent lifting of
the local variable, e.g.,

   oneCoin = commit [(\_ -> let x free in (coin x,x)) undefined]

However, this is neither intuitive nor reliable because an optimizing
compiler might transform this definition of oneCoin into the previous

Therefore, we need some other way to make committed choice available.
One option is to resurrect the old choice expression syntax (after
which commit seems to be modeled anyway):

   Expr ::= ... | ChoiceExpr
   ChoiceExpr ::= choice { ChoiceBranch_1 ; ... ; ChoiceBranch_n }
   ChoiceBranch :: Expr -> Expr [ where LocalDefs ]

With that syntax

   oneCoin = choice { coin x -> x where x free }

and it is clear that the variable x is local to the constraint and its
associated expression. However, this kind of choice expressions was
criticized for making it very difficult to implement a lazy merge

Another option is to change commit so as to take a list of unary
functions instead of a list of expressions:

   commit :: [a -> (Success,b)] -> a -> b

where commit applies all functions from the list to its second
argument and chooses one of the results for which the constraint
is satisfied without binding any non-local variables. (Obviously,
the pattern of that function must match commit's second argument.)
With this definition of commit one could define

    oneCoin = commit [\_ -> let x free in (coin x,x)] undefined

and lazy merge function

   merge l1 l2 =
     commit [\([],l2) -> (success,l2),
             \(l1,[]) -> (success,l1),
             \(e:r,l2) -> (success,e : merge r l2),
             \(l1,e:r) -> (success,e : merge l1 r)]

Since this is quite complicated, I would suggest providing some special
syntax for committed choice, which is similar to that of case

   Expr ::= ... | ChoiceExpr
   ChoiceExpr ::= choice Expr of { ChoiceBranch_1 ; ... ;
ChoiceBranch_n }
   ChoiceBranch :: Expr [ | Expr ] -> Expr [ where LocalDefs ]

With this syntax oneCoin and merge can be defined as follows:

   oneCoin = choice undefined of { _ | coin x -> x where x free }

   merge l1 l2 =
     choice (l1,l2) of
       ([],l2) -> l2
       (l1,[]) -> l1
       (e:r,l2) -> e : merge r l2
       (l1,e:r) -> e : merge l1 r



> BTW, as I already mentioned, I don't think that the primitives
> ensure... will be often use in application programs.
> In my applications it is sufficient to drop all evaluation
> annotations and add ensure... calls only in the Port library
> (where suspension is really necessary).

Don't forget appendix A.6 of the report :-)

[AH+02] E. Albert, F. Huch, M. Hanus, J. Oliver and G. Vidal.
         An Operational Semantics for Declarative Multi-Paradigm
         ENTCS76, 2002.

curry mailing list
Received on Do Dez 02 2004 - 17:37:41 CET

This archive was generated by hypermail 2.3.0 : Do Mai 23 2024 - 07:15:07 CEST