Re: [isabelle] Type variable names in inherited locales
On Mon, 11 Aug 2008, Peter Lammich wrote:
> When deriving a locale, say locale B = A + something, the type variables
> of A will be renamed to 'a,'b, ... for use in B. Can this behaviour be
> changed to keep the names of the type variables unless there are name
> clashes, or is there a good reason for this renaming ?
The reason for this is the regular ML type discipline, which produces most
general types on import of locale expressions into the new context. The
same happens when using polymorphic constants within a term, for example:
the locally bound type variables of the constant declaration are
instantiated to canonical fresh names according to the application
You have used the terminology of "deriving" locales above, and the example
B = A + something is reminiscant of class inheritance in o.o. language.
This model does not really fit to locales, although one could imagine a
different module system that comes closer to that expectation.
This archive was generated by a fusion of
Pipermail (Mailman edition) and