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
one.
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
function.
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)]
(l1,l2)
Since this is quite complicated, I would suggest providing some special
syntax for committed choice, which is similar to that of case
expressions.
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
Comments?
Wolfgang
P.S.:
> 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
Languages.
ENTCS76, 2002.
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Do Dez 02 2004 - 17:37:41 CET