Email Gateway (Aug 18 2022 at 17:31): Email Gateway (Aug 18 2022 at 17:31):From: ivanov@irit.fr
Hello,
Could you explain me, why in the following example, Isabelle 2011
accepts command value "id2 1", but refuses command value "id1 1"
(with message like "1 is incompatible with type 'a") ?
(-------------------------------------------------)
theory LocaleTest imports Main
begin
locale test_loc = fixes f :: "'a \<Rightarrow> 'a"
begin
fun id1::"'a \<Rightarrow> 'a" where "id1 x = x"
fun id2::"'b \<Rightarrow> 'b" where "id2 x = x"
value "id2 1"
value "id1 1"
end
end
(-------------------------------------------------)
Ievgen Ivanov
Email Gateway (Aug 18 2022 at 17:32):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear Ievgen,
the locale declaration in your example not only fixes the parameter f, but also
the type variable 'a. Thus, within the context test_loc, the type variable 'a is
treated like a fixed type name. Only when you interpret the context outside,
e.g. via an interpretation, does the 'a get generalised to a type variable and
instantiated as specified.
Hence, the 'a in the type declaration for id1 is no free type variable, whereas
'b is not bound in any context, so id2 has the polymorphic type 'b => 'b inside
the context.
By the way, there have been lately a number of posts on this mailing list on
Isabelle's polymorphims support.
Andreas
ivanov@irit.fr schrieb:
Last updated: Apr 24 2024 at 16:18 UTC