Re: [isabelle] Scala generator

On 02/03/2011 08:07 AM, René Thiemann wrote:
We have improved the Scala code generation to add parentheses around function literals as suggested,
and provide a fix as changeset 3450e57264b3 in the development version.

@Rene: I hope we can also identify and fix the other quirks with the Scala code generation; just provide us some further pointers.
Here is another one.

class class0 = fixes elem :: 'a
class class1 = class0
class class2 = class0
definition f :: "'a :: {class1, class2}" where "f \<equiv>  elem"
export_code f in Scala file "Problem.scala"

Then the file Problem.scala is created:

object Problem {

trait class0[A] {
   val `Problem.elem`: A
def elem[A](implicit A: class0[A]): A = A.`Problem.elem`

trait class1[A] extends class0[A] {

trait class2[A] extends class0[A] {

def f[A: class1: class2]: A = elem[A] /* line 14 */

} /* object Problem */

which does not compile:
Problem.scala:14: error: ambiguous implicit values:
  both value evidence$1 of type Problem.class1[A]
  and value evidence$2 of type Problem.class2[A]
  match expected type Problem.class0[A]
def f[A: class1: class2]: A = elem[A]

This can be only fixed by someone, who understands how type classes were thought to be modelled as implicits, i.e., our code generation guru Florian.

Florian's thoughts have been partly recorded on, but he can probably say more about this "diamond problem".



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