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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
