Re: Curry Report Vers. 0.8.2

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 Thu Mar 16 2006 - 18:42:34 CET

This archive was generated by hypermail 2.3.0 : Wed Sep 18 2019 - 07:15:05 CEST