*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions*From*: Christoph LANGE <math.semantic.web at gmail.com>*Date*: Tue, 02 Jul 2013 19:47:54 +0100*Organization*: University of Birmingham*Sender*: Christoph Lange <allegristas at gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130627 Thunderbird/17.0.7

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 -- 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/

object RealMinusBug { abstract sealed class nat final case class Zero_nat() extends nat final case class Suc(a: nat) extends nat trait minus[A] { val `RealMinusBug.minus`: (A, A) => A } def minus[A](a: A, b: A)(implicit A: minus[A]): A = A.`RealMinusBug.minus`(a, b) def minus_nata(m: nat, n: nat): nat = (m, n) match { case (Suc(m), Suc(n)) => minus_nata(m, n) case (Zero_nat(), n) => Zero_nat() case (m, Zero_nat()) => m } implicit def minus_nat: minus[nat] = new minus[nat] { val `RealMinusBug.minus` = (a: nat, b: nat) => minus_nata(a, b) } def minus_funa[A, B : minus](a: A => B, b: A => B, x: A): B = minus[B](a(x), b(x)) implicit def minus_fun[A, B : minus]: minus[A => B] = new minus[A => B] { val `RealMinusBug.minus` = (a: A => B, b: A => B, c: A) => minus_funa[A, B](a, b, c) } def broken: nat => nat => nat = (a: nat) => minus_funa[nat, nat => nat]((_: nat) => (_: nat) => Zero_nat(), (_: nat) => (_: nat) => Zero_nat(), a) } /* object RealMinusBug */

(* $Id: nVCG_CaseChecker.thy 1322 2013-07-02 15:05:55Z langec $ Auction Theory Toolbox Authors: * Christoph Lange <math.semantic.web at gmail.com> Dually licenced under * Creative Commons Attribution (CC-BY) 3.0 * ISC License (1-clause BSD License) See LICENSE file for details (Rationale for this dual licence: http://arxiv.org/abs/1107.3212) *) theory RealMinusBug imports Main begin definition broken :: "nat \<Rightarrow> nat \<Rightarrow> nat" where "broken = (\<lambda> b n . 0::nat) - (\<lambda> b n . 0::nat)" definition working2 :: "nat \<Rightarrow> nat" where "working2 = (\<lambda> b . 0::nat) - (\<lambda> b . 0::nat)" definition working1 :: "nat \<Rightarrow> nat" where "working1 = (\<lambda> n . 0::nat) - (\<lambda> n . 0::nat)" export_code broken in Scala module_name RealMinusBug file "code/RealMinusBug.scala" end

**Follow-Ups**:

- Previous by Date: [isabelle] Remaining uses of DVI files?
- Next by Date: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Previous by Thread: [isabelle] Remaining uses of DVI files?
- Next by Thread: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Cl-isabelle-users July 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list