Re: Type-classes and call-time choice vs. run-time choice

From: Juan Rodriguez Hortalá <juanrh_at_fdi.ucm.es>
Date: Fri, 28 Aug 2009 12:36:36 +0200

Hi Wolfgang, Sergio, and the rest of the list.

> For instance, one could extend the expression
> syntax with
>   BasicExpr ::= ... | ({ Expr }) | ...
> where an expression ({ e }) is evaluated with run-time choice.
> E.g., given
>   dbl x = x + x
>   main = dbl ({ 0 ? 1 }) =:= 1
> the goal main succeeds, which it doesn't with call-time choice.

In
my opinion the description "is evaluated with run-time choice" is not
very clear, because the values for '0 ? 1' are the same under call-time
choice and run-time choice. What you want is to express that the values
for '0 ? 1' will be "unshared" in the context where they are used, in
this case that the copies of the instance of 'x' made by 'dbl' will be
independent. In [1]
https://gpd.sip.ucm.es/trac/gpd/wiki/GpdSystems/RtToy#Run-timechoicebasedvariant
you can find a theoretical proposal and a "toy" implementation for a
combination of call-time choice and run-time choice based in annotating
functions as "call-time choice functions" or "run-time choice
functions", to indicate whether they perform sharing of their arguments
or not. In your example 'dbl' would be a run-time function. Maybe it
would be better having a call-time choice behaviour for every function
by default (if no annotations are provided for it) and allowing to
annotate, not only the functions, but its arguments separately, as
call-time or run-time arguments. This is also possible in the framework
of [1]. Then you could annotate "arbL2'" as "arbL2' is rt" or any
concrete syntax. This would be useful for class functions with
arguments, which would be expected to be shared, while the dictionary
argument will be unshared.

Maybe it could be interesting for you
the converse approach for combining call-time choice and run-time
choice of [2]
https://gpd.sip.ucm.es/trac/gpd/wiki/GpdSystems/RtToy#Call-timechoicebasedvariant.
The core language presented there, using the ^rt annotation after the
desugaring of Def. 1 (see paper pointed in [2]), uses the same idea you
propose, of expressing that some expressions will be "unshared". There
is also another prototype for it, but the resulting framework is not
very clean in my opinion.

On the other hand there are more
alternatives to call-time choice and run-time choice. One of these can
be found in [3]
https://gpd.sip.ucm.es/trac/gpd/wiki/PluralSemantics/Maude, the
prototype there also allows for mixing so called plural and singular
(call-time choice) arguments in the function.

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

Regarding
this changes of names, I prefer the old names call-time choice and
run-time choice because this is well established terminology, that is
used beyond the functional-logic community. But this is just an
opinion, as long as the semantics associated to each name is clear,
that is fine for me. Maybe classical rewriting and rewriting with
sharing are appropriated names too?, that is my proposal. But I must
insist that I am aware of at least two more alternatives to call-time
and run-time choice ([3] for example) caused by pattern matching,
henceforth the dichotomic approach to this nomenclature is rather
unfortunate, in my opinion.

Greetings,

Juan

 --
------------------------------------------------------------------------
Juan Rodríguez Hortalá
Grupo de Programación Declarativa / Declarative Programming Group
E-Mail : juanrh_at_fdi.ucm.es
Home Page: http://gpd.sip.ucm.es/juanrh/
Tel: + 34 913947646
Despacho / Office: 220 (2ª planta / 2nd floor)
Dept. Sistemas Informáticos y Computación / Department of Computer Systems and Computing
Universidad Complutense de Madrid
Facultad de Informática
C/ Profesor José García Santesmases, s/n
E - 28040 Madrid. Spain





_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Aug 28 2009 - 13:19:21 CEST

This archive was generated by hypermail 2.3.0 : Do Feb 01 2024 - 07:15:09 CET