[isabelle-dev] Countable instantiation addition
bulwahn at in.tum.de
Fri Jul 22 10:44:18 CEST 2011
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.
More information about the isabelle-dev