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

[Brian Huffman]

Quoting Makarius <makarius at sketis.net>:

> On Sat, 28 Feb 2009, Brian Huffman wrote:
>
>> If this is so, then maybe it is a good idea to move ATP_Linkup so that
>> it is imported by Plain? I know that some library theories import only
>> Plain and Presburger, for example; if ATP_Linkup were included with
>> Plain, it might avoid wasting resources in those cases.
>
> I've discussed that with Florian to some degree.  He made a good job in
> reorganizing the HOL theory graph, without having to include ATP_Linkup in
> Plain.

I'm a bit puzzled. Are you saying that it is actually better for  
ATP_Linkup *not* to be in Plain? Or is it just that Florian was able  
to save himself the work of moving it?

> Concerning the library, I am always puzzled why anything other than Plain
> or Main (or Complex_Main) is ever taken as a basis.

I can think of two separate reasons why someone might prefer using  
specific imports over just importing Main.

1. Accurately representing the library writer's intentions.

I don't think of Main as being all of one piece; my mental model is  
more like a disparate collection of libraries, some of which I may  
need, and others I may not. So if I write "imports Main", it really  
feels to me like I'm writing "imports List Map Presburger  
Relation_Power SetInterval Hilbert_Choice ..."

If I'm writing a library that actually uses a lot of those features,  
then "imports Main" is OK, it is good and concise. However, sometimes  
I write theories where I actively think about how many of the standard  
libraries are never used. It is mentally jarring to write "imports  
Main" when I am actually thinking "this theory doesn't use the List  
library". If minimal dependencies are part of the conscious design of  
a library, then that should be recorded in the source, and it is nice  
to have that statically checked, too.

2. Keeping clutter out of the name space.

When you say "imports Main", that brings a *lot* of constants and  
syntax into scope. And the number is growing all the time (I'm  
thinking of List.thy in particular). Name clashes are annoying,  
especially when the offending constant is not from a theory that you  
really needed to import anyway. Syntax clashes are even worse: You  
can't use qualifiers to disambiguate syntax like you can with constant  
names, and infix operators are in rather short supply. Minimizing  
imports tends to minimize problems with name space clashes.

- Brian