Re: [isabelle] Isabelle 2011 locales



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 at irit.fr schrieb:
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



--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft






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