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

[Florian Haftmann]

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
session.

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
	Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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>