[isabelle-dev] Countable instantiation addition

[Lukas Bulwahn]

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.


Lukas