Email Gateway (Aug 18 2022 at 12:17): Email Gateway (Aug 18 2022 at 12:17):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
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 current behaviour makes referring to type variables of imported
locales not really readable.
Currently, I'm inserting constrains-statements as a workaround, but this
may get tedious with many types or locales.
Example:
locale DPN =
fixes D :: "('Q\<times>'\<Gamma> list) set"
begin
(* Everything fine:
locale DPN =
fixes D :: "'Q \<times> '\<Gamma> list \<Rightarrow> bool"
*)
end
locale DPN1 = DPN
begin
(* Types renamed to 'a and 'b:
locale DPN1 =
fixes D :: "'a \<times> 'b list \<Rightarrow> bool"
*)
end
(* Workaround: *)
locale DPN2 = DPN +
constrains D :: "('Q\<times>'\<Gamma> list) set"
begin
(* Everything fine again:
locale DPN2 =
fixes D :: "'Q \<times> '\<Gamma> list \<Rightarrow> bool"
*)
end
Email Gateway (Aug 18 2022 at 12:17):From: Makarius <makarius@sketis.net>
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
Last updated: Nov 21 2024 at 12:39 UTC