Re: [isabelle] No tail-recursive code equation for List.map



>> Is it possible to enable code equations only for certain target
>> languages?

Definitely not at the moment.

As far I can see, there are now two issues (currying in Scala, tail
recursion) which would justify to differentiate code equations wrt. to
the target language.

Andreas Lochbihler a few months ago also showed funny surprises in
PolyML of obviously equivalent function definitions with dramatic
differences in runtime behaviour.

Before making any step ahead, it would be good to collect some general
observations which shapes of code equations are particularly suitable
for certain target languages, e.g.
* avoid Currying in languages which have bias towards tupled function
arguments (Scala)
* avoid tail recursion in lazy languages (Haskell)
* eta-expand certain function defintions (???)
* …

Once there is more certainty what could be done in that respect,
appropriate devices can be developed (different bins for code equations,
different preprocessor for certain target languages, …).

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.