- 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, 16 Mar 2006 18:19:03 +0100

Michael Hanus wrote:

*> Since there are changes at several places, in particular,
*

*> the redefinition of the evaluation annotations (eval flex/rigid
*

*> removed, ensureNotFree added etc), I have marked this version
*

*> as preliminary so that I can easily include any corrections
*

*> that I receive in the next days.
*

I have a few comments.

With regard to evaluation annotations, I think it was consensus

on this list to get rid of eval choice annotations, too, and

introduce a new primitive function commit for committed choice.

http://www.informatik.uni-kiel.de/~curry/listarchive/0297.html

In fact, I would find it odd if the report reserved two keywords

for a feature that isn't implemented in any of the existing Curry

implementations.

Furthermore, I found two places in the report where let-free

expressions are still restricted to constraints, namely:

- in Sect. 2.5 on p.10, the reports says that free declarations "can

occur in where-clauses or in a let enclosing a constraint". Instead

it should say that these declarations can occur in where-clauses and

in let expressions. Eventually, the whole sentence could be omitted.

- In the typing rules in Fig. 1 on p.21, the existential is still

restricted to type Success. Both occurrences of type Success

should be replaced by a type variable \tau'.

BTW, is there any reason for including the boolean conditional in

the typing rules? After all, according to the report an expression

if b then e1 else e2

is just syntactic sugar for the expression

Prelude.if_then_else b e1 e2

and therefore the typing of the conditional is implied by the

application rule.

In the prelude, I have been puzzled a bit by the somewhat complicated

definition of the operator ($##), which applies a function to an

argument that is evaluated to a ground normal form:

f $## x | x=:=y = y==y `seq` f y where y free

I would propose to add a new primitive function ground with type

signature

ground :: a -> a

to the prelude, which evaluates its argument to a non-variable head

normal form (like ensureNotFree) and also applies ground recursively

to all arguments of the result (if any). With that function, the

definition of ($##) becomes

f $## x = f $!! ground x

which IMHO expresses the intent of the operator in a much cleaner way

than the current definition. In addition, I also like the symmetry

between this definition and that of $#.

Furthermore, it is nice having a data type Ordering in the prelude,

but it would be more useful if there were also a compare function using

this type and it would be even more useful if this function had a

polymorphic type signature, i.e.

compare :: a -> a -> Ordering

MCC already defines this function and its user's guide also explains

the (quite obvious) result of compare when it is applied to two data

constructors.

If a polymorphic compare is added in this way, the definition of

Bool in the standard prelude should be changed into

data Bool = False | True

so that False `compare` True = LT as one would expect.

The operational semantics in appendix D still distinguishes flex and

rigid branch nodes in definitional trees. In particular, at the top of

p.74 in Sect D.1 where definitional trees are defined and at the bottom

of p.74 in the example tree for leq. Next is Fig.2 on p.75 where the

rule for

Eval[[e; branch(\pi,p,r,T_1,...,T_k)]]

should omit the r parameter and in its third case the condition r=flex.

Instead, the operational semantics should include the following rules

for ensureNotFree:

Eval[[c(e_1,...,e_n)]] => D

------------------------------------------

Eval[[ensureNotFree(c(e_1,...,e_n))]] => D

and

Eval[[f(e_1,...,e_n)]] => D

------------------------------------------------------------------------

-------------

Eval[[ensureNotFree(f(e_1,...,e_n))]] => replace(ensureNotFree(f

(e_1,...,e_n)), 1, D)

On p.80 in Sect. D.6 there are also still references to the evaluation

annotation modes, in the left hand side of the function gt, and in the

example tree at the bottom of the page.

Regards

Wolfgang

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Do Mär 16 2006 - 18:42:34 CET

Date: Thu, 16 Mar 2006 18:19:03 +0100

Michael Hanus wrote:

I have a few comments.

With regard to evaluation annotations, I think it was consensus

on this list to get rid of eval choice annotations, too, and

introduce a new primitive function commit for committed choice.

http://www.informatik.uni-kiel.de/~curry/listarchive/0297.html

In fact, I would find it odd if the report reserved two keywords

for a feature that isn't implemented in any of the existing Curry

implementations.

Furthermore, I found two places in the report where let-free

expressions are still restricted to constraints, namely:

- in Sect. 2.5 on p.10, the reports says that free declarations "can

occur in where-clauses or in a let enclosing a constraint". Instead

it should say that these declarations can occur in where-clauses and

in let expressions. Eventually, the whole sentence could be omitted.

- In the typing rules in Fig. 1 on p.21, the existential is still

restricted to type Success. Both occurrences of type Success

should be replaced by a type variable \tau'.

BTW, is there any reason for including the boolean conditional in

the typing rules? After all, according to the report an expression

if b then e1 else e2

is just syntactic sugar for the expression

Prelude.if_then_else b e1 e2

and therefore the typing of the conditional is implied by the

application rule.

In the prelude, I have been puzzled a bit by the somewhat complicated

definition of the operator ($##), which applies a function to an

argument that is evaluated to a ground normal form:

f $## x | x=:=y = y==y `seq` f y where y free

I would propose to add a new primitive function ground with type

signature

ground :: a -> a

to the prelude, which evaluates its argument to a non-variable head

normal form (like ensureNotFree) and also applies ground recursively

to all arguments of the result (if any). With that function, the

definition of ($##) becomes

f $## x = f $!! ground x

which IMHO expresses the intent of the operator in a much cleaner way

than the current definition. In addition, I also like the symmetry

between this definition and that of $#.

Furthermore, it is nice having a data type Ordering in the prelude,

but it would be more useful if there were also a compare function using

this type and it would be even more useful if this function had a

polymorphic type signature, i.e.

compare :: a -> a -> Ordering

MCC already defines this function and its user's guide also explains

the (quite obvious) result of compare when it is applied to two data

constructors.

If a polymorphic compare is added in this way, the definition of

Bool in the standard prelude should be changed into

data Bool = False | True

so that False `compare` True = LT as one would expect.

The operational semantics in appendix D still distinguishes flex and

rigid branch nodes in definitional trees. In particular, at the top of

p.74 in Sect D.1 where definitional trees are defined and at the bottom

of p.74 in the example tree for leq. Next is Fig.2 on p.75 where the

rule for

Eval[[e; branch(\pi,p,r,T_1,...,T_k)]]

should omit the r parameter and in its third case the condition r=flex.

Instead, the operational semantics should include the following rules

for ensureNotFree:

Eval[[c(e_1,...,e_n)]] => D

------------------------------------------

Eval[[ensureNotFree(c(e_1,...,e_n))]] => D

and

Eval[[f(e_1,...,e_n)]] => D

------------------------------------------------------------------------

-------------

Eval[[ensureNotFree(f(e_1,...,e_n))]] => replace(ensureNotFree(f

(e_1,...,e_n)), 1, D)

On p.80 in Sect. D.6 there are also still references to the evaluation

annotation modes, in the left hand side of the function gt, and in the

example tree at the bottom of the page.

Regards

Wolfgang

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Do Mär 16 2006 - 18:42:34 CET

*
This archive was generated by hypermail 2.3.0
: Fr Sep 30 2022 - 07:15:05 CEST
*