[isabelle-dev] A better policy for the typerep class
brianh at cs.pdx.edu
Sat Feb 28 22:07:03 CET 2009
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
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.
More information about the isabelle-dev