[isabelle-dev] A better policy for the typerep class

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Wed Feb 11 08:47:48 CET 2009

Dear all,

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



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090211/608cd0ba/attachment.sig>

More information about the isabelle-dev mailing list