[isabelle-dev] Code export to Haskell and lower-case theory names

[Makarius]

On Fri, 29 Mar 2013, Joachim Breitner wrote:

> Hi,
>
> Am Freitag, den 29.03.2013, 15:32 -0700 schrieb Brian Huffman:
>> On Fri, Mar 29, 2013 at 10:40 AM, Joachim Breitner <breitner at kit.edu> wrote:
>>> Am Freitag, den 29.03.2013, 13:24 +0100 schrieb Makarius:
>>>>> This has got nothing to do with Isabelle's informal conventions but is
>>>>> all about the target language's formal rules.
>>>>
>>>> The conventions about theory names and locale/class names are not that
>>>> informal.  If you violate them systematically, certain name space policies
>>>> will break down.  That is then a "general user error".
>>>
>>> Are there really things that break if I deviate from the convention?
>>
>> The main problem I know about is that qualified names can become
>> ambiguous: e.g. if "foo.bar.baz" and "bar.boo.baz" are both in scope,
>> then "bar.baz" could refer to either of them. The problem is avoided
>> if theory names and locale/type/constant names are kept disjoint. See
>> also this old thread:
>>
>> https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2011-July/001674.html
>
> but in every case there is a more qualified name that can be used to
> identify each entity? I would not consider that a hard problem, just an
> annoyance. I read this as “if you deviate from the suggested scheme,
> things might become a little bit less convenient, but everything still
> works” which I find fair enough.

When name spaces were introduced in 1998 and locales in 1999, the people 
behind all that (including myself) looked very carefully what can be 
achieved with minimal extra complexity.  The result of that was to keep 
theory names always capitalized and locales lower-case, in accordance to 
what was established practice for a long time already.  This very simple 
scheme allows to refer to the outer two levels of the name space hiearchy 
and the reliably without extra worries.

Otherwise, certain name accesses can become inaccesible, which I would 
call more that just inconvenient, especially since the whole name space 
business has become a bit more complex in the years after 2005.


So far there were no reasons given on this thread why the convention 
should not be followed first place.  Are there any?


 	Makarius