[isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions



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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.