Email Gateway (Aug 18 2022 at 18:48): Email Gateway (Aug 18 2022 at 18:48):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi René,
1.) It is in someway possible to make the generated code have an
explicit export list? So something likeexport_code bla foo [export] in Haskell module_name Code file -
that results in the following module definition
module Code (bla, foo) where ...?
The reason is, that w/o an explicit export list the compiler assumes
that all functions are exported and therefore does not inline them or
uses other code optimizations (see [1]).
this is an interesting observation. Up until now, I did not pay much
attention to export lists, in order to keep things as simple as
possible. So far I did not consider inlining issues. There are
important enough to reconsider hiding and exporting anew. Anyway,
analysis and implementation will take considerable time.
2.) I noted that when using "Efficient_Nat", I got two new types for
natural numbers in code: Natural and Nat. The code of both looks nearly
identical (see attached files) and also only one of them (Nat) is used
throughout the rest of the code. Is there a deeper reason behind having
them both?
Consider type classes: there is only one instantiation of a type per
class; this prohibits to map two different types in the logic onto the
same type in Haskell. This affects all languages with implicit
dictionaries, i.e. also Scala, but not SML/Ocaml.
Cheers,
Florian
Email Gateway (Aug 18 2022 at 18:48):From: René Neumann <lists@necoro.eu>
Am 12.12.2011 13:03, schrieb Florian Haftmann:
Hi René,
1.) It is in someway possible to make the generated code have an
explicit export list? So something likeexport_code bla foo [export] in Haskell module_name Code file -
that results in the following module definition
module Code (bla, foo) where ...?
The reason is, that w/o an explicit export list the compiler assumes
that all functions are exported and therefore does not inline them or
uses other code optimizations (see [1]).this is an interesting observation. Up until now, I did not pay much
attention to export lists, in order to keep things as simple as
possible. So far I did not consider inlining issues. There are
important enough to reconsider hiding and exporting anew. Anyway,
analysis and implementation will take considerable time.
This sounds like you plan on adding some sort of automated generation of
export lists. Would be as hard to implement some additional syntax that
gives the user the choice of specifying the export list that is going to
be generated (I don't know though whether this concept is useful for the
other languages...)? Just to avoid having to edit auto-generated files.
2.) I noted that when using "Efficient_Nat", I got two new types for
natural numbers in code: Natural and Nat. The code of both looks nearly
identical (see attached files) and also only one of them (Nat) is used
throughout the rest of the code. Is there a deeper reason behind having
them both?Consider type classes: there is only one instantiation of a type per
class; this prohibits to map two different types in the logic onto the
same type in Haskell. This affects all languages with implicit
dictionaries, i.e. also Scala, but not SML/Ocaml.
Thanks for the explanation.
Email Gateway (Aug 18 2022 at 18:53):From: René Neumann <lists@necoro.eu>
Hi,
I have two questions regarding the Haskell-code generation in Isabelle
2011-1:
1.) It is in someway possible to make the generated code have an
explicit export list? So something like
export_code bla foo [export] in Haskell module_name Code file -
that results in the following module definition
module Code (bla, foo) where ...?
The reason is, that w/o an explicit export list the compiler assumes
that all functions are exported and therefore does not inline them or
uses other code optimizations (see [1]). For my test-case this makes
indeed a huge difference:
without export list:
benchmarking fully 200
collecting 100 samples, 1 iterations each, in estimated 33.55970 s
mean: 337.4847 ms, lb 336.8887 ms, ub 338.2864 ms, ci 0.950
std dev: 3.518088 ms, lb 2.850222 ms, ub 5.044390 ms, ci 0.950
with export list:
benchmarking fully 200
collecting 100 samples, 1 iterations each, in estimated 30.92251 s
mean: 103.9187 us, lb 99.45309 us, ub 119.4683 us, ci 0.950
std dev: 37.75363 us, lb 11.42921 us, ub 84.93836 us, ci 0.950
Note the difference of 300ms vs. 0.1ms.
2.) I noted that when using "Efficient_Nat", I got two new types for
natural numbers in code: Natural and Nat. The code of both looks nearly
identical (see attached files) and also only one of them (Nat) is used
throughout the rest of the code. Is there a deeper reason behind having
them both? Or is it the result of some refactoring and forgetting to
remove the old version?
Thanks :)
René
Nat.hs
Natural.hs
Last updated: Nov 21 2024 at 12:39 UTC