Re: [isabelle] New AFP theory: List Index



On 22/02/2010, at 8:10 PM, Florian Haftmann wrote:

>> A feature that I often miss, especially considering namespace pollution
>> problems. One of the top-candidates on my wish list
>> is something like import-qualified, giving the user control over what
>> symbols (and syntax) will be loaded into the toplevel-namespace.
> 
> This is a misunderstanding which exhibits the source of the problem:
> syntax is not bound to namespaces but always global, which makes
> pollution pervasive (c.f. the funny (no_)notation declarations for inf
> and sup in the HOL theories -- an Isabelle joke...). We need finer
> control over syntax here.

Yes, we do. 

We don't need to do everything at once, though. We'd still be in a well-defined, better state if we could just treat normal names (thms, consts, types) in theory name spaces.


>> Currently, the hide-command allows one to hide
>> private symbols, but the other way round would be more comfortable.
> 
> I do not seed this demand as urgent: given that theory developers have
> thought carefully which symbols ought to be hidden / qualified, the user
> is always free to hide additional symbols when needed.

This requires the user to know everything in the libraries (and track all syntax changes over library versions). Much better to be able to import only what you want. 

In our project we have really bad cases of name space pollution (three large specifications describing the same thing, names do get scarce quickly). The conceptual problem is long solved in other languages. We "just" need to implement one of the solutions.


>> If users want hierarchical module names, why don't we (the Isabelle
>> developers) just implement that feature?
> 
> I agree that this is desirable.  But I suppose we first should find a
> way to replace the rather archaic session concept by something which is
> less driven by building descriptions in IsaMakefiles and ROOT.MLs, but
> by the implicit structure of hierarchies.

I see that as a fairly orthogonal problem (not that it shouldn't be addressed at some point). The sessions really only govern what theories get loaded when. All actual dependencies and data are tracked on the theory level by Isabelle already anyway. I'd rate proper name spaces a much higher priority.


> A somehow related question is how to treat relative imports.  I recall
> there has been (still is?) much debate on this in the Java and Python
> community, and this has to be considered carefully (maybe inspired by
> Scala!?).

In terms of name space handling, I so far like the Haskell model best. This is something that can easily be discussed and tweaked, though (almost as hard as concrete syntax ;-))). The real problem will be down at the technical end as Makarius writes.

Cheers,
Gerwin






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.