Re: Evaluation Annotations (Was Re: Proposal: Relaxing restrictions in Curry

From: Wolfgang Lux <wlux_at_uni-muenster.de>
Date: Fri, 05 Nov 2004 12:09:10 +0100

Bernd Brassel wrote:

> Without wishing to open up an old topic again: What were the reasons
> to make seq rigid? Why should it not correspond to head normal form?
> You could always define the old seq as
> oldseq x y = case x of _ -> y
> or does that taste too much like a hack?

No, not like a hack, but it will not work as you expect. The expression
case x of _ -> y is equivalent to let _ = x in y and since there is no
demand for x in that expression, it simply does not evaluate x at all.
At least this is what Haskell implementations and MCC do and I think
this
is also what the Curry report says:
   The informal operational meaning of the case expression is as follows.
   Evaluate e so that it matches a pattern p_i.
Since there is only one pattern and every expression matches e, there is
no need for evaluating e. In fact, the reason that one cannot use
   case x of _ -> y
in order to force x's evaluation was my original motivation for
proposing
the seq function, and since case was rigid it appeared to me that seq
should be rigid as well, which I not realize was some kind of
short-circuit.

> Subsuming, I would agree to Wolfgang's proposal to eliminate eval
> annotations. I would avoid, however, to introduce a new rigid
> primitive and express rigidity by case expressions.

First of all, unless the Curry report does explicitly clarify that
case x of _ -> y *does* evaluate x, you cannot define a polymorphic
function rigid with type a -> a. [BTW, note that there is a good
reason for not evaluating x in that case expression because it
destroys the property that you can rewrite
   case x of c p1 ... pk -> e
into
   case x of c x1 ... xk -> case x1 of p1 -> ... -> case xk of pk -> e
where x1,...,xk are fresh variables and p1,...,pk are patterns.]

Even if this change were made, I propose to have a rigid function in
the prelude
because it is too useful. With the help of that function, you can
define oldseq
simply by oldseq = sed . rigid, which is so simple that I don't think it
deserves to become a prelude function (unless someone really has a need
for it).

Another use of rigid (since you were asking for something like that in
another
posting) could be ensuring that the arguments of a message stream are
not
variables: map rigid . rigidSpine.

In fact, one could take this idea a step further and also provide a
primitive
function ground :: a -> a, which (again lazily) ensures that its result
is a
ground term, i.e.,
   ground X = ground (rigid X)
   ground (C e1 ... ek) = C (ground e1) ... (ground ek)
where X is an unbound variable, and C is a constructor of arity k.
(Obviously,
this will have to be a primitive except in an implementation using type
classes,
where one could automatically derive ground). On the other hand, I once
implemented this function for MCC (it is available as Success.ground),
but
it turns out that I do not use it because it seems to be too rigid, so
I'm
not sure how useful this function would really be (at least for sending
message
through ports it certainly isn't).

Regards
Wolfgang


_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fri Nov 05 2004 - 16:49:20 CET

This archive was generated by hypermail 2.3.0 : Mon Sep 16 2019 - 07:15:05 CEST