Email Gateway (Aug 22 2022 at 09:27): Email Gateway (Aug 22 2022 at 09:27):From: Julian Brunner <julianbrunner@gmail.com>
Dear all,
I recently stumbled upon the following behavior in Isabelle which I
find surprising and which affects me negatively. In the attached
theory, the constant "bar" is defined in the locale "foo". This locale
is then interpreted as "baz" using a 'for' clause to retain the
parameter "f".
I had expected that "baz.bar" would be "% f. foo.bar f 0" :: "('a =>
'b) => 'b". Instead, it is "% type f. foo.bar f 0" :: "'a itself =>
('a => 'b) => 'b". Why is there a type parameter, given that the type
variable "'a" is already determined by the parameter "f"? It seems
that Andreas Lochbihler has already stumbled upon the same issue
(https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2010-April/msg00029.html),
but it did not get any replies. It seems that everything works when I
instantiate the parameter "type" with "TYPE('a)", but I would prefer
if I didn't have to do that.
Regards,
Julian
TypeParameter.thy
Email Gateway (Aug 22 2022 at 09:41):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Julian,
this is an instance of the problem of hidden polymorphism, which is
difficult to deal with in the presence of arbitrary interpretation
morphisms.
The phantom parameter you experience will vanish immediately if the 'a
parameter is instantiated to a fixed type.
Florian
signature.asc
Last updated: Apr 25 2024 at 08:20 UTC