[isabelle-dev] Scala implicits

[Manuel Eberl]

Looks good. After applying the patch, HOL-Codegenerator_Test goes 
through with the code equation in Binomial.thy enabled.


Cheers,

Manuel


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.
>
>
> Cheers,
>
> Manuel
>
>
> 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.
>>
>> Cheers,
>>     Florian
>>
>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>>