[isabelle-dev] A better policy for the typerep class
florian.haftmann at informatik.tu-muenchen.de
Wed Feb 11 08:47:48 CET 2009
I think there are different aspects which we should clearly set apart.
a) Keeping theory imports minimal vs. reducing the number of merges
Careful thinking what the logical preliminaries of a particular theory
are is a necessary, valuable and fruitful task -- I would by no means
encourage to develop the HOL theories as a structureless coagulation.
That, in order to reduce the number of merges, there are some
recommended "wasp-waists" in the HOL theory dependencies, does only
superficially conflict with this: add the appropriate import (Plain,
Main) to the theory if necessary, and the job is done. When a
rearranging of theories is to be done, the proper minimal imports are
reconstructible quite easily -- in the worst case using an interactive
b) The type-class instance problem in general
> However, as the Haskell community long recognized, the real problem is
> still lurking ahead. If two different users (or developers of libraries)
> each provide their own class instances for A :: B, then their theories
> are now incompatible. They cannot be merged, and it is impossible for
> any third party to use their theories together at the same time. This is
> no minor inconvenience; it is actually impossible to overcome without
> modifying and restructuring the two theories involved.
Here everything has been said by Brian already.
c) The typerep problem in particular
I also agree that automated instance in general are more a timed bomb
than a support. However the instantiation of typerep conceptually is
just supposed to be an extension of typedef. Due to bootstrap reasons
(which can be changed, as I pointed out in an earlier e-mail) typerep is
only available since List/Main. If typerep would go before Plain (as
can be done as I have written in an earlier e-mail), that problem would
be resolved since after Plain the instantiation of typedefs to typerep
would follow immediately, leaving no room for duplicated instances.
Hope this helps
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 252 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev