[isabelle-dev] Scala implicits

[Florian Haftmann]

> Florian, what are you plans w.r.t. merging this patch into the
> distribution?

It's currently on the testboard.

	Florian

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

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160623/a09a3ba9/attachment.sig>