Re: [isabelle-dev] Countable instantiation addition
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...) Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Countable instantiation addition
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
Re: [isabelle-dev] Countable instantiation addition
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Countable instantiation addition
On 07/21/2011 09:47 PM, Gerwin Klein wrote: The idea has potential for generalisation. Could we turn this into something similar to Haskell's deriving? The command would take a datatype and a list of instantiation methods that each know how to instantiate a datatype for a specific type class, e.g. enum, countable, order, etc. An instantiation method would be basically a usual proof method plus some small part that knows how to set up the specific instantiation goal (probably the same code for pretty much all applications of this) plus some background theory that provides the basic setup. I like this approach. You ask for something explicitly and then you get it, but you don't have to remember a new obscure syntax for every bit of it. You would just write datatype foo = deriving countable, finite, Several existing things fit into this scheme: When I define a fresh datatype foo = Bar in Main, it automatically becomes an instance of the following type classes: - equal (executable equality, for code generation) - term_of(reifiable term structure, for code generation) - size (size function, for termination proofs) - full_exhaustive(for exhaustive quickcheck) (there is actually a large zoo of type classes for quickcheck...) This doesn't mean that we have to make every last thing explicit, but a mechanism would make sense. Note that in general, a proof method is not enough, since we have to define overloaded constants. Here, countable is an exception since the class has no parameters. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
