Email Gateway (Aug 19 2022 at 10:48): Email Gateway (Aug 19 2022 at 10:48):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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)
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
signature.asc
Email Gateway (Aug 19 2022 at 10:49):From: Brian Huffman <huffman@in.tum.de>
"Avoid tail recursion" is not good general advice for Haskell!
Tail-recursive implementations are preferred for many Haskell
functions, especially those that always consume the entire input
before they can produce any output. For example, "sum :: [Int] -> Int"
is best as tail-recursive. Functions like "map" and "[m..n]" are
implemented without tail recursion so that they can produce output
incrementally.
A better rule of thumb for Haskell is that for functions that return
lazy datatypes, equations with a lazy constructor surrounding any
recursive calls are preferable.
Email Gateway (Aug 19 2022 at 10:59):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,
I had similar problems when processing large files using generated
code for Scala, where I did exactly the same as Cornelius did for some
similar function to map.
However, this optimization is clearly language-dependent, because
in Haskell I don't want to have the tail-recursive version, e.g.
consider the call
take 5 (filter f (map g long_list))
So, if there will be a tail-recursive code equation for List.map in
the default library, please only activate it on languages which
really profit from tail-recursion.
Best regards,
René
Email Gateway (Aug 19 2022 at 10:59):From: Peter Lammich <lammich@in.tum.de>
Is it possible to enable code equations only for certain target
languages?
Email Gateway (Aug 19 2022 at 10:59):From: Brian Huffman <huffman@in.tum.de>
I remember having a similar thought when I saw the changeset "tail
recursive code for function upto" a while back.
http://isabelle.in.tum.de/repos/isabelle/rev/a019e013b7e4
The original (non-tail recursive) code would be preferred when
generating Haskell.
Email Gateway (Aug 19 2022 at 10:59):From: René Thiemann <rene.thiemann@uibk.ac.at>
Here is at least one possible solution:
consts scala :: bool
code_const scala
(Haskell "False")
(Scala "true")
(SML "false")
(OCaml "false")
(Eval "false")
(* tail recursive variant for Scala to reduce Stack-size at the cost of double traversion *)
definition
remove_comments :: "string => string"
where
"remove_comments = (if scala then rev o (remove_comments_tail_rec []) else remove_comments_standard)"
Kind regards,
René
Email Gateway (Aug 19 2022 at 11:13):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian,
Andreas Lochbihler a few months ago also showed funny surprises in
PolyML of obviously equivalent function definitions with dramatic
differences in runtime behaviour.
For completeness, here are the figures that I had mentioned to you. I have tested
different code equations for fold on a red-black tree with 100 000 000 entries from theory
HOL/Library/RBT_Impl.
The equation for Empty is always the same
fold f rbt.Empty = id
but I tried three versions for the branch case:
a) fold f (rbt.Branch c l k v r) = fold f r ◦ f k v ◦ fold f l
b) fold f (rbt.Branch c l k v r) = (λb. fold f r (f k v (fold f l b)))
c) fold f (rbt.Branch c l k v r) b = fold f r (f k v (fold f l b))
Under PolyML, I got the following timings, i.e., the eta-expanded version performed best.
a) 0.54 s
b) 0.38 s
c) 0.15 s
Andreas
Last updated: Apr 20 2024 at 12:26 UTC