[isabelle-dev] typrep?

[Alexander Krauss]

Brian Huffman wrote:
> I, for one, am rather alarmed at the hurdles that Amine was forced to 
> overcome to do a simple merge of two theories.

I agree.

> I think that the automatic class-instantiations should be disabled 
> immediately, and replaced with a new top-level command so that these 
> instantiations can be done explicitly, and individually.

In fact, "typerep" is not the only class that is instantiated 
automatically. Another one is "size", which is also of a technical 
nature. But it never posed problems, I think, because it is installed 
early enough that everybody inherits from it.

I think that automatic class instantiations are acceptable provided that
a) the class is for "internal" use of some tools and manual 
instantiation is discouraged, and b) The mechanism is installed early 
enough to avoid the merge issue.

IMO the options are

1) Make the whole Typerep theory optional, to be loaded together with 
the Imperative HOL theories.

2) Typerep provides a top-level command for generating the instantiations.

3) Move Typerep up the hierarchy, such that it is always present and 
there are no merge problems.

Note that 1 and 2 do not actually solve the problem but only limit it to 
theories that use Imperative HOL (in 1) or the top-level command (in 2). 
I think I nevertheless prefer option 1, since Typerep is really a 
specialized thing.

The cleanest, but also the hardest solution would be to make class 
instances "applicative" instead of "generative" (I may be streching the 
terms a bit far here), such that equal class instances do *not* collide 
at a later merge.

Alex