[isabelle-dev] Countable instantiation addition

[Lukas Bulwahn]

On 07/22/2011 10:44 AM, Lukas Bulwahn wrote:
> On 07/22/2011 09:36 AM, Alexander Krauss wrote:
>>> datatype foo = ....
>>> deriving countable, finite,
>>
>> Tobias also mentioned "set_of", "map_of", etc. But since these aren't 
>> class instantiations (we have no constructor classes such as 
>> "functor"), we end up with the good old generic datatype 
>> interpretation (roughly: datatype -> theory -> theory).
>>
>> So it seems like we simply want named datatype interpretations that 
>> are explicitly invoked via "deriving" (stretching the original 
>> Haskell notion quite a bit...)
>>
> Yes, this was my first goal for the "deriving" project, creating a 
> nice user interface and providing  a "implementation guide" for 
> datatype interpretations, and automatic type class instantiations, 
> which would end up as "recipe" in the Isabelle Cookbook.
>
> A second goal was to automatically derive the interpretation by asking 
> the user to give the definitions for some examples (as this can also 
> be done in Haskell).
>
> Of course, the student would have to have a strong ML background and 
> must learn a lot about data types. Therefore, I wrote the project idea 
> down, even if such a prospective student might never exist.
>
I forgot to mention that the "deriving" project I was talking about was 
one of the project ideas for this year's Google Summer of Code, which 
was not chosen to be completed.


>
> Lukas
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>