[isabelle-dev] Scala implicits
eberlm at in.tum.de
Thu Jun 23 11:22:53 CEST 2016
Looks good. After applying the patch, HOL-Codegenerator_Test goes
through with the code equation in Binomial.thy enabled.
On 23/06/16 09:48, Manuel Eberl wrote:
> The uncommented code equation at the end of ~~/src/HOL/Binomial.thy used
> to break Codegenerator_Test. I can have a look later to see whether this
> is still the case.
> If it is not, we should probably proceed to move some more of René
> Thiemann et al's efficient code equations from the AFP to the distribution.
> I'm glad to see this (hopefully) resolved.
> On 23/06/16 09:45, Florian Haftmann wrote:
>> Dear power users of code generation to Scala,
>> during the last months there have been some reports on ambiguity
>> problems with implicits in Scala.
>> One kind of these has been known for long and can be addressed in more
>> recent versions of Scala, which has been done in 7cffe366d333.
>> One other kind is presumably resolved with the patch attached,
>> applicable to b3e5bdb784f5. The key idea is to generate implicits in
>> Scala (stemming from type class instances) into the respective companion
>> objects of corresponding type classes.
>> Since I have no example at hand where such ambiguities have been
>> observed to happen, I would kindly ask whether someone might try whether
>> that patch resolves the issue. No problems on the visible theory
>> universe (Isabelle distribution plus AFP) have been encountered.
>> The patch still keeps the traditional Scala approach that each implicit
>> dictionary holds all operations of all super classes. I don't know
>> whether this is still apt to expose problems, but this could be tackled
>> in a second step.
>> Thanks to Lars Hupel for suggesting these solutions.
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
More information about the isabelle-dev