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

[Brian Huffman]

Hello,

I have been thinking about all the conflicts caused by the typerep  
class, and what should be done about it.

Basically, this is an instance of a more general problem. The Isabelle  
libraries define some types, and they also define some type classes.  
The problem, stated simply, is where should the class instances go?

The Haskell community has been dealing with this issue for a long  
time. The Haskell standard libraries are extensive, with a much wider  
variety of types, classes, and instances than Isabelle's libraries  
have. Yet they have done a much better job managing all of that  
complexity than we are doing at the moment with the typerep class.

We would do well to learn some things from the Haskell community about  
organizing class instances in libraries, specifically:

1) Exactly what problems arise when standard libraries don't have  
class instances set up properly, and

2) What policies actually work to avoid such problems.

I'll start with point 1. Here's the scenario: An Isabelle user imports  
two theories, both of which are part of the standard distribution.  
Theory A defines a type A, and theory B defines a type class B, but  
there is no instance for A :: B anywhere in the distribution. The most  
immediate problem for the user is the lack of the class instance; to  
remedy this, he will have to provide it himself. For a class like  
typerep, this is actually really easy; the missing class instance is  
at most a minor inconvenience.

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.

The important point here is that *merging theories* is our main  
concern. Users can deal with missing instances, but if users do not  
have the ability to merge theories, then our efforts have failed.

Keeping this in mind, it is clear that Florian's new "feature" that  
automatically generates typerep class instances is seriously  
misguided. It solves the minor inconvenience of missing instances, but  
at the same time, it totally destroys all future potential for merging  
theories. I'm sure that Florian had the best intentions, but his  
automatic-instance mechanism is a complete failure with respect to the  
deeper problem caused by missing instances - namely, the inability to  
merge theories.

OK, now for point 2. What should our policy be? Clearly, if the  
standard library defines a type A and a class B, and a suitable  
instance for A :: B exists, then the instance must also be included  
somewhere in the standard library. In the case of the typerep class,  
this means every type defined in the Isabelle/HOL image must also have  
a typerep instance in the Isabelle/HOL image.

The next question is where (within the distribution) should the  
instances go? In the Haskell libraries, the policy is that every  
instance should reside in one of two places: 1) in the same module as  
the type definition, or 2) in the same module as the class definition.  
This is a reasonable policy, and it would probably work for Isabelle.  
However, it would also be reasonable in Isabelle to allow instances to  
reside in a theory separate from either the type or class definitions.  
(This situation is discouraged in Haskell for performance reasons with  
GHC.) Following the Haskell policy tends to create a linear theory  
dependency graph (with lots of "wasp-waists"), so it might be better  
to split things up more to create more opportunities for parallelism.  
Policy decisions like this should be discussed further.

- Brian