In order to add run-time choice to Curry programs, Wolfgang suggests
that one could annotate
expressions or constructors. Juan proposes to annotate functions.
I would like to add a thought that there is another entity in Curry
programs which might be a good position for annotations: variables.
I just take Wolfgang's syntax {...} for some examples I take from
Wolfgang's mail:
Assume again that
> > class Arb a where
> > arb :: a
> > instance Arb Bool where
> > arb = False ? True
Is translated to
> > data Arb' a = Arb' ({-arb::-} a)
> > arb' (Arb' f) = f
> > inst'Arb'Bool = Arb' arb'Bool
> > arb'Bool = False ? True
and
> > arbP2 = (arb,arb)
> > arbL2 = [arb,arb]
to
> > arbP2' da db = (arb' da, arb' db)
> > arbL2' da = [arb' da, arb' da]
My suggestion for the resulting functions with the meaning intended by
Wolfgang would be
> arb' (Arb' {f}) = f
and
> arbP2' {da} {db} = (arb' da,arb' db)
> arbL2' {da} = [arb' da, arb' da]
While I agree with Juan that the {...} annotation of expressions does
not seem to lead to a concept where it is always clear what the
results should be, the same is not true with the annotation of
variables. In a recent paper we have proposed a semantics based on
equations where four type annotations are allowed on variables:
Val (for value), PVal (for partial value), Ch (for choices over
partial value) and Exp (for arbitrary expressions) and there is a
subtyping relation Val < PVal < Ch < Exp.
As usual, the types simply express what set of values the variable can
be substituted with. For example assume that the variable "da" of
arbLs above is of type
Ch. Then it may be substituted with (Arb' (0?1)) (which is of type Ch)
but not with, e.g.,
(Arb' (double coin)) which is of type Expr. If the variable is of type
PVal like the "x" in your usual "double x = ..." it may not be
substituted with (0?1), but only with 0 and with 1, respectively.
I think that this is all really a consequent extension of the CRWL-
idea (with a bit of algebraic polish).
If you uniformly use the same type annotation for _all_ variables in
the program you get a different meaning overall:
Val leads to call-by-value
PVal leads to call-by-need with call-time choice
Ch leads to call-by-need with run-time choice (sorry, Sergio.)
Exp leads to call-by-name, i.e., expressions may be evaluated more
than once.
By construction the type annotations can also be mixed freely. In
addition to the call-time, run-time discussion of this thread, mixing
in the other types can also be useful:
Val, e.g., for integration of external functions or where laziness is
too slow
Exp can be very useful for examples where laziness needs to much memory.
Maybe you want to have a look at:
www-ps.informatik.uni-kiel.de/~bbr/papers/OrderSortedFLP.pdf
Greeting
Bernd
Am Aug 28, 2009 um 9:40 AM schrieb Wolfgang Lux:
> Hi Sergio,
>
>> There is an interaction between the order of evaluation and the
>> run-time choice. Incidentally, "run-time" is a bad choice (sic!)
>> of name, since the call-time choice occurs at run-time as well;
>> better names are eager choice and lazy choice.
>
> You are right, run-time choice is probably a bad name, I will
> use eval-time choice henceforth. I don't think that eager and
> lazy choice are good names because they are easily confounded
> with eager and lazy evaluation. To make things worse, eager
> choice matches what is commonly understood as lazy evaluation,
> i.e., non-strict evaluation with sharing a.k.a. call-by-need.
>
>> In your example "dbl", if you want the lazy choice, but evaluate
>> (0 ? 1) a bit early, you will not get the value 1, hence you will
>> not get the lazy choice.
>
> Indeed, the interaction between call-time choice (sharing) and
> eval-time choice (no sharing) is rather subtle. In my example
> a compiler might notice that the body of dbl always evaluates
> its argument and hence evaluate the argument eagerly before the
> call. But then, the compiler must not evaluate an expression of
> the form ({ e }) eagerly because this could introduce some
> unintended sharing as shown by the example.
>
> Problems like this are the reason why I'd prefer the restricted
> proposal where eval-time choice is used only for specially marked
> arguments of data constructors. In that case, both the function
> which applies a data constructor and the function which matches
> the data constructor know about the eval-time choice semantics.
>
> Wolfgang
> _______________________________________________
> curry mailing list
> curry_at_lists.RWTH-Aachen.DE
> http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Aug 28 2009 - 18:15:11 CEST