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

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.


	Makarius





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