- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: Wolfgang Lux <wlux_at_uni-muenster.de>

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

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 Thu Dec 02 2004 - 17:37:41 CET

Date: Thu, 02 Dec 2004 14:20:35 +0100

Michael Hanus wrote:

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.:

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 Thu Dec 02 2004 - 17:37:41 CET

*
This archive was generated by hypermail 2.3.0
: Thu Nov 14 2019 - 07:15:05 CET
*