[isabelle-dev] typrep?

[Tobias Nipkow]

Now that I'm beginning to understand what typerep is, I most certainly 
agree that it is too specialized to force it on everybody.

Tobias

Alexander Krauss wrote:
> 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
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev