[isabelle] Scala code generator generates ill-typed code ... · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Scala code generator generates ill-typed code ...

Email Gateway (Aug 19 2022 at 11:24):

From: Christoph LANGE <math.semantic.web@gmail.com>
Dear Isabelle developers,

I would like to report a bug in Scala code generation.

(BTW, is the Scala code generator actively maintained? That would be
great, because our main selling point in using Scala as an output target
is to demonstrate that such code can easily be integrated with
business-ready software. This is work in the context of formalising
auctions, see
http://www.cs.bham.ac.uk/research/projects/formare/code/auction-theory/,
so we need to convince people who may never heard of SML, OCaml and
Haskell, but have heard of Java.)

Please find attached:

RealMinusBug.thy: a minimal example in which I tracked down the bug.
Please don't take the filename seriously; it's just that initially I
thought the bug was related to real numbers.
RealMinusBug.scala: just to be sure: the Scala code Isabelle 2013
generates from this

Here is the problem:

--- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< ---
$ scalac -version
Scala compiler version 2.10.1 -- Copyright 2002-2013, LAMP/EPFL
$ scalac RealMinusBug.scala
RealMinusBug.scala:26: error: overriding value RealMinusBug.minus in
trait minus of type (A => B, A => B) => A => B;
value RealMinusBug.minus has incompatible type
val RealMinusBug.minus = (a: A => B, b: A => B, c: A) =>
^
one error found
--- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< ---

I am not yet a Scala expert, so this leaves me clueless.

As the *.thy demonstrates the problem is somehow caused by doing a
"minus" operation on functions whose types have a certain complexity.
When the functions have simpler types, the "function subtraction"
generates correctly typed Scala code, as demonstrated by the working*
definitions in the *.thy file.

If you wonder why I need these lambda-abstractions in my definitions at
all, please bear in mind that my actual formalisation is more complex.
Actually I have something like

fun bar :: "type1 => type3 => type4"
where "bar a c = (* something lengthy *)"

fun baz :: "type1 => type2 => type3 => type4"
where "baz a b c = (* something lengthy *)"

fun foo :: "type1 => type2 => type3 => type4"
where "foo a b c = bar a - baz a b"

i.e. the function foo that creates the problem subtracts two partially
applied functions.

I managed to work around this by generating code from a modified function

fun foo_workaround
where "foo_workaround a b c =
(* expansion of bar *)
-
(* expansion of baz *)"

Cheers,

Christoph
RealMinusBug.scala
RealMinusBug.thy

Email Gateway (Aug 19 2022 at 11:25):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christoph,

Concerning »actively maintained«, there is somebody (namely me) who will
look after your issue. I welcome your effort to carry Isabelle out of
the ML/Haskell subculture, but there is one caveat: the code generator
for Scala translates HOL's calculus into a functional Scala program
without attempting any transformation to idiomize it towards Scala as
written by experienced Scala programmes. For illustration, have a look
at the generated code. I never heard of any reports how feasible the
code is to incorporate in bigger Scala applications.

Stay tuned,
Florian
signature.asc

Email Gateway (Aug 19 2022 at 11:26):

From: "C. Diekmann" <diekmann@in.tum.de>
BTW,

(BTW, is the Scala code generator actively maintained?

As a regular user of the Scala code generator for over a year, I can
tell that I am very happy and that it _feels_ very maintained.

I never heard of any reports how feasible the
code is to incorporate in bigger Scala applications.

I have >8k LOC Scala application with interactive visualization,
command tab completion and some other nifty features from third party
libraries (not counted in the LOC). The core reasoning logic (> 2.5k
LOC) is generated by the code generator. It is very feasible. You do a
great job! The transition form Isabelle 2012 / Scala 2.9 to Isabelle
2013 / Scala 2.10 was quite painless. However, I really recommend
using an object oriented facade to wrap the generated Scala code
before usage with hand-written Scala.

[...] )
(see xkcd 859)

Cornelius

Email Gateway (Aug 19 2022 at 11:26):

From: Christoph LANGE <math.semantic.web@gmail.com>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hi Florian,

2013-07-03 19:33 Florian Haftmann:

Concerning »actively maintained«, there is somebody (namely me)
who will look after your issue.

Thanks for your encouraging reply!

And, @Cornelius, thanks for your experience report.

I welcome your effort to carry Isabelle out of the ML/Haskell
subculture, but there is one caveat: the code generator for Scala
translates HOL's calculus into a functional Scala program without
attempting any transformation to idiomize it towards Scala as
written by experienced Scala programmes.

I am nowhere near an _experienced_ Scala programmer yet, but
sufficiently capable of writing wrapper functions that, e.g., convert
set[Nat] to List[Int], so this is fine with me. Replying to
@Cornelius, my application so far is small enough to only require a
few wrapper _functions_, but I'll consider your suggestion of doing
something object-oriented.

Are you suggesting that the code generator creates nicer output for
other target languages? (I'm just curious; I'm not planning to use
any other language than Scala for now.)

For illustration, have a look at the generated code. I never
heard of any reports how feasible the code is to incorporate in
bigger Scala applications.

For now, our applications won't be more than thin wrappers around the
generated code, providing some console or file I/O, in a medium-term
perspective maybe a GUI or web interface. But really just to obtain
input for the Isabelle-generated functions from an end user, and for
displaying the output of the Isabelle-generated functions back to the
end user.

Cheers,

Christoph

Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Intelligent Computer Mathematics, 8–12 July, Bath, UK.
http://cicm-conference.org/2013/
→ Modular Ontologies (WoMO), 15 September, Corunna, Spain.
Submission until 12 July; http://www.iaoa.org/womo/2013.html
→ Knowledge and Experience Management, 7-9 October, Bamberg, Germany.
Submission until 15 July; http://minf.uni-bamberg.de/lwa2013/cfp/fgwm/
→ Mathematics in Computer Science Special Issue on “Enabling Domain
Experts to use Formalised Reasoning”; submission until 31 October.
http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.20 (GNU/Linux)
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

iEYEARECAAYFAlHUm5kACgkQvqg+op3jsjNJDgCg6hhflHW3bCwVRAaw9HbJ4anu
TiwAnjjsYpuIpT4WGPu/gN0NhzktAmup
=adh6
-----END PGP SIGNATURE-----

Email Gateway (Aug 19 2022 at 11:26):

From: Manuel Eberl <eberlm@in.tum.de>
At the danger of being called a nitpicker: this sort of thing can cost
you the programme correctness that you have so painstakingly ensured
with Isabelle, since Int in Scala is subject to integer overflow. I have
heard stories of "verified" code producing horribly wrong results
because people did not take integer overflow into account. These stories
were from code verified with a verification condition generator and
automated theorem provers; the Isabelle-generated code is, of course,
not affected by things like this, but when writing wrappers around it
that use native integer types, the same caveats apply.

Personally, unless I do some heavy number-crunching, I use the
arbitrary-precision Integer type (in Haskell) just to be sure –
especially with Isabelle-generated code.

Cheers,
Manuel

Email Gateway (Aug 19 2022 at 11:26):

From: Christoph LANGE <math.semantic.web@gmail.com>
2013-07-03 23:38 Manuel Eberl:
Thanks for pointing out. Indeed BigInt would be the right type to use
in Scala.

Cheers,

Christoph

Email Gateway (Aug 19 2022 at 11:26):

From: Makarius <makarius@sketis.net>
The funny thing is that the type called "Int" or "int" in most real-world
programming languages is not for integers at all, but for machine words.

The JVM platform is in a relatively good situation here, because that is
precisely specified as 32bit signed word-arithmentic. So overflow is not
an accident, but part of the algebra on that particular type. (There are
also celebrated books about making really smart things with that algebra
of words.)

Surprise only starts, when people use that word type as approximation for
proper ints. There are historical and technical reasons for doing that by
default on the JVM: BigInt is much less efficient on that platform, due to
the physical distinction of base types vs. object types at runtime.

In SML the situation is much better: type "int" means mathematical
integers, without implicit overflow, and the implementation is quite fast:
for small values it uses fast machine arithmentic, for big values it
silently upgrades to a library (here GNU MP, which is also quite fast).

Makarius

Email Gateway (Aug 19 2022 at 11:27):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,

I have identified the issue; it will not show up in the next Isabelle
release.

The issue occurs whenever there is a class parameter of type … => 'a,
and a corresponding dictionary is needed for a function type instance.
Maybe there is a chance to work around this in your application. If
not, and there is pressure not to await the upcoming release, it would
be possible to provide the necessary adjustions as dedicated patches (we
do not do this often, but sometimes there is no directer way).

Cheers,
Florian
signature.asc

Email Gateway (Aug 19 2022 at 11:27):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Cornelius,

thanks for this encouraging report!

Florian
signature.asc

Email Gateway (Aug 19 2022 at 11:27):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Interfacing with generated code requires indeed some care. E.g. the
generated code does not prevent you from generating abstract values
which do not obey the required invariant. Clean encapsulated interfaces
are helpful here.

Florian
signature.asc

Email Gateway (Aug 19 2022 at 11:27):

From: Christoph LANGE <math.semantic.web@gmail.com>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hi Florian,

2013-07-05 18:29 Florian Haftmann:

I have identified the issue; it will not show up in the next
Isabelle release.

Great, thank you very much!

The issue occurs whenever there is a class parameter of type … =>
'a, and a corresponding dictionary is needed for a function type
instance. Maybe there is a chance to work around this in your
application.

Indeed there is: I had already found a workaround when reporting the
bug; the workaround is sketched at the bottom of my initial email. So
there is no need for a custom patch, at least not from my side.

Cheers,

Christoph

Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

iEYEARECAAYFAlHXYkIACgkQvqg+op3jsjNpogCgsuH2r1e5AAVKu+6VwJcz/uqf
KzgAn0HA2yvyLcAf1Pb/dqK0a4tiJ+mY
=jwla
-----END PGP SIGNATURE-----

Last updated: Apr 19 2024 at 12:27 UTC