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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
