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.


ivanov at schrieb:

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
locale test_loc = fixes f :: "'a \<Rightarrow> 'a"

fun id1::"'a \<Rightarrow> 'a" where "id1 x = x"
fun id2::"'b \<Rightarrow> 'b" where "id2 x = x"

value "id2 1"

value "id1 1"


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 - 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.