Email Gateway (Aug 18 2022 at 09:33): Email Gateway (Aug 18 2022 at 09:33):From: Peter Lammich <peter.lammich@uni-muenster.de>
Sorry if I posted this question already a few month ago:
Having a locale with two parameters
locale A =
fixes X :: "'a"
fixes Y :: "'a"
I want to derive a locale from that, where the type of the parameters is
constrained, for example:
locale B = A +
constrains X :: "'a list"
this will result in the error message:
*** exception TYPE raised: unify_parms: failed to unify types ?'a and 'b
*** At command "locale".
Whereas
locale B = A +
assumes "False ==> X = (X::('a list))"
as well as
locale B = A +
constrains X :: "'a list"
constrains Y :: "'a list"
gives the expected result. Is there any reason for the first declaration
to fail ?
The second one is obviously a "dirty hack", while the 3rd one can be
tedious to write down if having many fixed parameters with related types.
Greeting and thanks in advance for any hints
Peter Lammich
Email Gateway (Aug 18 2022 at 09:34):From: Clemens Ballarin <ballarin@in.tum.de>
On 1 Aug 2006, at 13:57, Peter Lammich wrote:
Is there any reason for the first declaration to fail ?
The reason is, of course, rooted in the implementation. Unlike
assumes, constrains elements currently don't fully participate in type
inference. This phenomenon should disappear eventually.
The second one is obviously a "dirty hack", while the 3rd one can be
tedious to write down if having many fixed parameters with related
types.locale B = A +
constrains X :: "'a list"
constrains Y :: "'a list"
You shouldn't worry about this too much. There are not many examples
of useful locales where parameter types are instances of another
locale, and that do not have any additional assumptions.
(Endomorphisms vs. Homomorphisms is one.)
Clemens
Last updated: May 03 2024 at 12:27 UTC