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

[Makarius]

On Sat, 28 Feb 2009, Brian Huffman wrote:

> >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

Well, this is the main point of "Main".  In the better times of the HOL 
image, it was the one and only entry point for anything else.  
Applications (including libraries) did not worry about the bootstrap 
process of HOL.

Due to Main getting a bit bloated, we had to come up with a second 
stepping stone: Plain.  Moreover, since real/complex stuff is now also 
part of the same image, there are further theories above Main.


> 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.

This is indeed a fundamental problem.  Presently we have only half-baked 
workarounds, like no_notation or "hide const ...".

At some later stage, name space handling might get a substantial reform, 
but it is stuck with many "features" that have accumulated over time.

Making syntax subject to name spaces is even more difficult -- 
interestingly the Scala people have given up on that idea altogether.  
Nonetheless, I could imagine to have at least infixes managed in a more 
systematic way, not just collections of grammar productions.


	Makarius