[isabelle-dev] Countable instantiation addition
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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev