Email Gateway (Aug 19 2022 at 16:30): Email Gateway (Aug 19 2022 at 16:30):From: Ferdinand Vesely <csfvesely@swansea.ac.uk>
Dear mailing list,
I'm trying to develop a theory using modular records built from smaller
records in an arbitrary way. That is, I don't want to have to commit to
the order right at the beginning by using the "+" notation for
extending records. This seems to be partly achievable but has
limitations in that, e.g., selectors are not applicable. For example, I
define the component records:
record out = out :: string
record env = env :: "(string * val) list"
I can then define operations on these smaller records that carry over
to the bigger ones, e.g. a notion of composition:
class composable =
fixes compose :: "'a => 'a => 'a" (infix ";;" 60)
instantiation unit :: composable
begin
definition compose_unit_def:
"u1 ;; u2 = ()"
...
instantiation out_ext :: (composable) composable
begin
definition compose_out_def:
"r1 ;; r2 =
(| out = (out r1) @ (out r2), ... = (out.more r1) ;; (out.more
r2) |)"
...
instantiation env_ext :: (composable) composable
begin
definition compose_env_def:
"r1 ;; r2 = (
if (env r1 = env r2) then
(| env = env r2, ... |) = (env.more r1) ;; (env.more r2) |)
else undefined)"
...
Now I can have values of combined record types ("env out_ext" or "out
env_ext"), e.g.
value "(| out = ''abc'', env = [ (''x'', v) ] |)"
I can apply the overloaded operations to such values:
value "(| env = [ (''x'', v) ], out = ''abc'' |) ;;
;; (| env = [ (''x'', v) ], out = ''def'' |)"
and I can also select the first element:
value "out (| out = ''abc'', env = [ (''x'', v) ] |)"
However, since the selector for, e.g., env is only defined on "'a
env_scheme", I cannot apply it if env is not the first element in the
record:
value "env (| out = ''abc'', env = [ (''x'', v) ] |)"
Is there a way to select any element from such mix-and-match records?
If this is currently not possible, is there an inherent limitation in
the underlying ML implementation of records? I've had a brief look at
"HOL/Tools/record.ML" but didn't have much time to dive into it yet.
It is possible to define an overloaded selector using via type classes
(see attached theory), but this seems too much work.
Alternatively, I think it would also be interesting to have a more
general record definition construct, such as:
record out = ...
record env = ...
record big_record = out + env + ...
which would have the effect of:
record out = ...
record env = out + ...
record big_record = env + ...
My example theory is attached.
Kind regards,
Ferdinand
RecordsExample.thy
Email Gateway (Aug 19 2022 at 16:31):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Hello Ferdinand.
You have an interesting idea there. I have to warn you that interesting
ideas to improve the record package come up from time to time, and are
usually resolved to be too much work.
It would be possible to use class-based polymorphism to allow all
accessors and updators to apply to all relevant record constructions no
matter what order they were constructed in. That would complicate the
formal definitions quite a bit, and the record package is already quite
complicated. There would also remain the fundamental limit that records
can only be constructed as a linear composition of record extensions,
whereas I think some users would like to be able to merge a binary pair
of record environments.
It might be of interest to you to point out that Norbert Schirmer fought
with these restrictions a while ago, and came up with an approach in
which the record type, updators and accessors are simply introduced in a
locale. The locales can then be combined in any manner desired. The
final obligation (left until the proof is complete and assembled) is to
show that the hypothesised super-record, updators and accessors exists.
This only needs to be done once.
I think that the code in the Isabelle repo in "src/HOL/Statespace/"
implements this, but I might be confused about that.
Good luck!
Cheers,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 19 2024 at 20:15 UTC