Re: Evaluation Annotations: are they needed?

From: Julio Mariño y Carballo <jmarino_at_fi.upm.es>
Date: Mon, 15 Nov 2004 13:19:58 +0100

El Lunes, 15 de Noviembre de 2004 10:57, Michael Hanus escribió:
> I also think it is problematic to find an appropriate set of
> functions. At least, it would increase the complexity of the definition
> of the language. On the other hand, with Wolfgang's proposal one could
> define the rigidness projections as any other function (and put
> some important examples, like ensureSpine, into the prelude)
> and write instead of "f eval rp1 ... rpN"

I was also thinking of leaving this open to the programmers. The projections
more likely to be used, like the spine one would go in a standard prelude
(perhaps in "the" standard one) and those on user-defined types somewhere
else.

> I agree with Julio that it is useful to see the possible
> rigidness requirements of a function at some place.
> However, this need not to be done in the program code.
> For instance, the documentation of a function is usually
> a good place where this information could be shown.

My view is that the type declaration, the evaluation annotation and other
kinds of annotations (e.g. those for expressing demand) are actually part of
the documentation -- in fact a "hard" part, as they affect the compilation
process -- which must be completed with a "soft" part which includes natural
language explanations, and other constraints that might not be checkable or
inferred automatically.

> As a concrete example, look at the documentation of the PAKCS
> libraries at http://www.informatik.uni-kiel.de/~pakcs/lib/.
> This documentation is automatically generated, i.e., it is not
> a burden to the programmer, and it contains some useful information that
> is derived by analysing the program code. For instance, in the
> documentation of the concatenation function (++) at
>
> http://www.informatik.uni-kiel.de/~pakcs/lib/CDOC/prelude.html#++
>
> you will find the comment that (++) is "solution complete, i.e.,
> able to compute all solutions".

Very nice!!

By the way, if the solution completeness property was inferred automatically
via program analysis (and a trivial analyzer based on a sticky bit is not
difficult to imagine) then I see no problem in making that part of the hard
documentation, i.e. giving the appropriate warnings at compile time and
allowing the programmer to declare a given function as solution complete.

[Are you using the trivial sticky bit algorithm or a more ellaborate one? In
the latter case, where is it explained?]

> In a similar way, one could
> also add information about rigidness requirements.
> A non-standard type system might be useful to derive such information.
> We have used a similar approach to derive non-determinism information,
> i.e., we have defined "non-determinism types" for functions.

Which type system are you using for the determinism types? Are you considering
making it into the standard?

> A similar approach for rigidness is a challenge but might be possible.
> Regards,
>
> Michael

Best regards,

Julio



_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mon Nov 15 2004 - 13:23:21 CET

This archive was generated by hypermail 2.3.0 : Mon Nov 11 2019 - 07:15:06 CET