[isabelle-dev] A better policy for the typerep class
brianh at cs.pdx.edu
Tue Feb 10 21:16:54 CET 2009
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
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
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.
More information about the isabelle-dev