[isabelle-dev] Scala implicits
eberlm at in.tum.de
Thu Jun 23 13:17:00 CEST 2016
Florian, what are you plans w.r.t. merging this patch into the distribution?
On 23/06/16 11:22, Manuel Eberl wrote:
> 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
>> 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
>>> 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
>>> 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