I agree with Gerwin. Records are datatypes. Hence one should be able to
pattern match against them as in FP languages. The record package can
arrange for this very easily via rep_datatype. On performance: I
recently came across an example of a short ML function with very
complicated pattern matching (no records) that took polyML one minute to
compile. Even the best systems have performance limits. Our standard
solution is the one Gerwin suggested.
Tobias
On 01/07/2011, at 2:16 PM, Makarius wrote:
On Fri, 1 Jul 2011, Thomas Sewell wrote:
The 'ext' constant, which constructs the (| a = 1, b = 2 |) style syntax, looks
like it's been there a while. Assuming this syntax is used in the future, it
will probably be backed by a constant. Naming it as a constructor would seem
reasonable, but I have no idea what the ramifications would be. I don't know
anything at all about the internals of the datatype package.
The only concern I can see is a potential performance problem with the datatype
package - there are some very large records in use. At least one, anyway. I did
consider at one point adding a flag which would turn off some features of the
package for users concerned about performance. This would make it easier to add
new features in if needed.
[..]
This merely illustrates that if there is anything worse than a lot of features it is
feature variants. E.g. we used to have certain options in datatype, and it
made Florian Haftmann's code generation on top of it incredibly difficult. So we spent
some efforts to remove such variants from datatype again, to get back to some sanity.
I agree that feature variants by options are problematic, they tend to explode
in number.
To add some data to the discussion, I've measure runtime of the rep_datatype
one-liner that Alex proposed. Things look good in the beginning, but the
datatype package does not scale well (have not measured memory usage):
100 fields:
12s record definition
2.35s rep_datatype
200:
57.6
23.14
300:
138.537
95.827
400:
347.242
342.078
500:
643.64
3421.79
For more than 500 fields this doesn't look feasible any more. Not sure if this
hit some memory bound on my machine, I was in a meeting when the test was
running, but even the trajectory up to 400 does not promise anything good
beyond 400.
There is of course the slightly evil option of checking for size and just not
do the rep_datatype for very large records (with warning emitted). It's not
even without precedent, lots of other packages have limits where they give up
on things, and the matching syntax at least only makes sense for smaller
records anyway.
Making the syntax available for matching would fit naturally into the
Isabelle/HOL as programming language paradigm that people have been propagating
for a while..
Cheers,
Gerwin
___
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
