[isabelle-dev] Countable instantiation addition

Lukas Bulwahn bulwahn at in.tum.de
Fri Jul 22 11:04:40 CEST 2011

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 

More information about the isabelle-dev mailing list