Re: [isabelle] New AFP theory: List Index



On Sun, Feb 21, 2010 at 12:55 AM, Peter Lammich
<peter.lammich at uni-muenster.de> wrote:
> Tobias Nipkow wrote:
>> A complication is that Isabelle does not support hierarchical module
>> names in the way Haskell (or Java or ...) does.
>>
> A feature that I often miss, especially considering namespace pollution
> problems.

If users want hierarchical module names, why don't we (the Isabelle
developers) just implement that feature?

The implementation wouldn't involve much:

1. Make the dot "." a legal character in module names.

2. Define a new mapping from module names to filepaths, so that
"imports A.B.C" makes Isabelle load the file "~/A/B/C.thy", where "~"
is filled in with some directory from the search path.

The hard part would be social, rather than technical: Deciding how to
organize and populate the hierarchy. But we wouldn't have to switch
over everything at once---we could flesh out the hierarchy gradually,
with input from the user community, and move libraries to their new
places in the namespace one at a time. I think this would work, and
solving the problem of module name clashes would remove one big
obstacle to sharing Isabelle libraries.

- Brian





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