Email Gateway (Aug 18 2022 at 17:28): Email Gateway (Aug 18 2022 at 17:28):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi all,
recently I tried to embed some generated code more deeply into the
Haskell standard library (by using Prelude functions whenever possible).
The initial problem (which many of you may know) is that whenever in
Isabelle you are using "nat" the corresponding Haskell function would
use either Int or Integer... since many Prelude functions are using Int,
lets just assume that Int should replace "nat" (ignoring the fact that
nat's may get arbitrarily large but Int's don't).
First HOL/Library/Efficient_Nat.thy seemed exactly to be what I needed,
but unfortunately it doesn't seem to hold what is claimed in the header:
"The efficiency of the generated code can be improved
drastically by implementing natural numbers by target-language
integers. To do this, just include this theory."
I did just import Efficient_Nat.thy, is there anything else to do
afterwards (maybe for Haskell Integers are used instead of Int's?).
Does anybody have experience with using Efficient_Nat for Haskell
code-generation?
cheers
chris
A minor comment: the code-generator setup for Haskell (in HOL.thy)
declares "&&" and "||" as infixl, whereas in Haskell's Prelude they are
declared infixr.
Email Gateway (Aug 18 2022 at 17:28):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear Christian,
Efficient_Nat does implement nat in terms of Haskell Integer, so the comment is
not wrong - provided you import Efficient_Nat as the last theory in your
import list in the theory where you invoke the Haskell code generator. Even if
you have imported Efficient_Nat in some ancestor theory, reimport it.
However, nat is not literally translated to Integer, but wraps Integer in a type
Nat (cf. the generated Nat.hs). This seems necessary to do because otherwise
type class instantiations could not be Isabelle-specific, e.g., division by 0 is
defined in Isabelle whereas not on Haskell integers. See also the comment in
Efficient_Nat on this.
The easiest way to use the Haskell standard library is probably to unpack Nat to
Integer via toInteger and to wrap it back via fromInteger whenever this is
needed in your custom translations.
If you wish to replace Integer by Int, you will have to rewrite Efficent_Nat.thy
to use Int in all Haskell translations.
Possibly, Florian can tell you more on that topic.
Andreas
Email Gateway (Aug 18 2022 at 17:29):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,
A minor comment: the code-generator setup for Haskell (in HOL.thy)
declares "&&" and "||" as infixl, whereas in Haskell's Prelude they are
declared infixr.
thanks for pointing that out, this seems to have been wrong from the
very beginning. Fixed in the hg repository (rev b992c8e6394b).
First HOL/Library/Efficient_Nat.thy seemed exactly to be what I needed,
but unfortunately it doesn't seem to hold what is claimed in the header:
"The efficiency of the generated code can be improved
drastically by implementing natural numbers by target-language
integers. To do this, just include this theory."I did just import Efficient_Nat.thy, is there anything else to do
afterwards (maybe for Haskell Integers are used instead of Int's?).
Well, for Haskell indeed Integers are used for consistency. But if your
code involves massive computation on considerably large nats,
Efficient_Nat should bring a considerable speedup. Maybe the bottleneck
is somewhere else? A clear statement requires an inspection of the
corresponding code.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 17:29):From: Lukas Bulwahn <bulwahn@in.tum.de>
Hello Christian,
we also provide the type code_numeral for Integers (Haskell Integer) for
code generation, cf. src/HOL/Code_Numeral.thy
Currently, in development, I added a type code_int that I map to bounded
Integers (Haskell int), cf. src/HOL/Library/Quickcheck_Narrowing.thy
But I developed the necessary theory about code_int only as far as I
needed it for my purpose.
I am aware that the code generation setup for code_int could be
potentially unsound, if you exploit overflows in some tricky way.
By this replacement, I have measured an overall 50% speed-up by
replacing Integer by Int in my setting, the speed-up in the replaced
parts must be even larger.
But from my experience, foreseeing or estimating possible performance
increases in Isabelle's generated code is a difficult task.
E.g., it is still unclear to me, if the resulting non-overlapping code
equations from overlapping sequential function definitions make a
measurable performance difference in the runtime of the generated code.
Of course, these dedicated types code_numeral and code_int are for some
very special purposes, evaluation by code generation, with ML, nbe and
quickcheck, in the system.
They do not provide much theorems to reason about them, and should be
chosen with care.
Hope this helps.
Lukas
Email Gateway (Aug 18 2022 at 17:29):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Thanks for all your fast answers,
just for clarification, I want to use Haskell's Int in order to be able
to map many functions to Prelude functions (like mapping List.length ::
'a list => nat to length :: [a] -> Int). I'm aware that this might lead
to inconsistencies (as Lukas already pointed out) -- not only because of
potential overflows but also since you cannot be sure that the Prelude
implementation is correct -- but for the time being I just wanted to be
able to do it anyway :)
In the end I'm thinking of a "safe" version of the generated code and a
"fast" version (using Int's and Prelude functions wherever possible).
It seems as if what Lukas has developed is exactly what I was searching
for. But first I will thoroughly read through the code-generation manual
(again) ;)
cheers
chris
Email Gateway (Aug 18 2022 at 17:29):From: Lukas Bulwahn <bulwahn@in.tum.de>
On 03/31/2011 10:56 AM, Christian Sternagel wrote:
Thanks for all your fast answers,
just for clarification, I want to use Haskell's Int in order to be
able to map many functions to Prelude functions (like mapping
List.length :: 'a list => nat to length :: [a] -> Int). I'm aware that
this might lead to inconsistencies (as Lukas already pointed out) --
not only because of potential overflows but also since you cannot be
sure that the Prelude implementation is correct -- but for the time
being I just wanted to be able to do it anyway :)In the end I'm thinking of a "safe" version of the generated code and
a "fast" version (using Int's and Prelude functions wherever possible).It seems as if what Lukas has developed is exactly what I was
searching for. But first I will thoroughly read through the
code-generation manual (again) ;)
If this is of general interest, I am happy to move this development into
a separate theory and incorporate your contributions. But I think we
should discuss all the gory details offline.
Lukas
cheers
chris
On 03/31/2011 10:36 AM, Lukas Bulwahn wrote:
Hello Christian,
we also provide the type code_numeral for Integers (Haskell Integer) for
code generation, cf. src/HOL/Code_Numeral.thyCurrently, in development, I added a type code_int that I map to bounded
Integers (Haskell int), cf. src/HOL/Library/Quickcheck_Narrowing.thy
But I developed the necessary theory about code_int only as far as I
needed it for my purpose.
I am aware that the code generation setup for code_int could be
potentially unsound, if you exploit overflows in some tricky way.By this replacement, I have measured an overall 50% speed-up by
replacing Integer by Int in my setting, the speed-up in the replaced
parts must be even larger.But from my experience, foreseeing or estimating possible performance
increases in Isabelle's generated code is a difficult task.
E.g., it is still unclear to me, if the resulting non-overlapping code
equations from overlapping sequential function definitions make a
measurable performance difference in the runtime of the generated code.Of course, these dedicated types code_numeral and code_int are for some
very special purposes, evaluation by code generation, with ML, nbe and
quickcheck, in the system.
They do not provide much theorems to reason about them, and should be
chosen with care.Hope this helps.
Lukas
On 03/31/2011 09:48 AM, Andreas Lochbihler wrote:
Dear Christian,
Efficient_Nat does implement nat in terms of Haskell Integer, so the
comment is not wrong - provided you import Efficient_Nat as the last
theory in your import list in the theory where you invoke the Haskell
code generator. Even if you have imported Efficient_Nat in some
ancestor theory, reimport it.However, nat is not literally translated to Integer, but wraps Integer
in a type Nat (cf. the generated Nat.hs). This seems necessary to do
because otherwise type class instantiations could not be
Isabelle-specific, e.g., division by 0 is defined in Isabelle whereas
not on Haskell integers. See also the comment in Efficient_Nat on this.The easiest way to use the Haskell standard library is probably to
unpack Nat to Integer via toInteger and to wrap it back via
fromInteger whenever this is needed in your custom translations.If you wish to replace Integer by Int, you will have to rewrite
Efficent_Nat.thy to use Int in all Haskell translations.Possibly, Florian can tell you more on that topic.
Andreas
Last updated: Apr 27 2024 at 04:17 UTC