Email Gateway (Aug 18 2022 at 15:28): Email Gateway (Aug 18 2022 at 15:28):From: John Matthews <matthews@galois.com>
Hi Florian,
I was demoing the code generator here at Galois, and someone wanted to
see what kind of Haskell code was generated for overloaded arithmetic.
We tried this example:
theory Int_ex
imports Main Code_Integer
begin
definition
"foo (x::'a::{number,plus,times}) y = x + 2 * y"
export_code foo in Haskell
module_name Int_ex
file "IntCode"
It was able to generate Haskell code, but the code itself is very
strange:
module Int_ex where {
class Plus a where {
plus :: a -> a -> a;
};
class Times a where {
times :: a -> a -> a;
};
class Number a where {
number_of :: Integer -> a;
};
foo :: forall a. (Plus a, Times a, Number a) => a -> a -> a;
foo x y =
plus x (times (number_of (error "Bit0" (error "Bit1" (error
"Pls")))) y);
}
Notice that in the definition of foo uses the "error" function and
Isabelle's internal datatype for integers. I had hoped the Haskell
definition would instead be:
foo x y =
plus x (times (number_of 2) y);
Should I be including a different adaptation theory here?
Thanks,
-john
smime.p7s
Email Gateway (Aug 18 2022 at 15:28):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi John,
the number class in Isabelle/HOL is a little bit arcane; concerning
code generation, you may use numerals on numeric types (nat, int, rat,
real), but not polymorphic ('a::number). Otherwise you only get
formally and partially correct code:
In typical Isabelle/HOL specifications, the number class will not show
up that often since it is only syntactic -- a classical joke is that you
cannot prove "2 + 2 = (4::'a::number)". Of more relevance is the class
number_ring which describes structures in which the integers can be
embedded semantically (number_of = of_int). This you can use to
circumvent the number_of problem: instead of
definition double :: "'a::number_ring ⇒ 'a" where
"double k = 2 * k"
write
definition double :: "'a::number_ring ⇒ 'a" where
"double k = of_int 2 * k"
Since (number_of = of_int), you can even prove the second version from
the first. This could also be done by the preprocessor but would
require writing a simproc since the naive rewrite (number_of k = of_int
(number_of k)) does not terminate.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 15:29):From: John Matthews <matthews@galois.com>
Hi Florian,
I'd like to stay with just the "syntactic" number, plus, etc. classes,
since our Haskell number instances don't necessarily satisfy the ring
axioms. So I can generate reasonable Haskell code from this Isabelle
definition:
definition
"foo (x::'a::{number,plus,times}) y = x + number_of 2 * y"
However I don't want to have to insert "number_of" functions wherever
I'm using a numeric literal. But right now I don't see any way of
generating reasonable Haskell code from this more readable version of
the above definition:
definition
"foo (x::'a::{number,plus,times}) y = x + 2 * y"
Is there any way to get the code generator to work well on this second
form?
Thanks,
-john
smime.p7s
Email Gateway (Aug 18 2022 at 15:29):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi John,
the inherent problem here is that the Isabelle and Haskell concept of
numeral is quite different. In the attached theory I have spelled out
what is the best possible solution I can imagine for this discrepancy
using the preprocessor:
a) For instances of number_ring, a substitution number_of k ~> of_int
(number_of k) is used.
b) For other polymorphic numeral expressions, the class number_num can
be used which can be provided with custom instances; then a substitution
number_of k ~> num_of (number_of k) can be applied.
I'm not quite sure whether this solves your problem, but if yes I will
include this into library (or even the Code_Integer theory).
Cheers,
Florian
Number.thy
signature.asc
Last updated: Apr 26 2024 at 08:19 UTC