Re: [isabelle] Additional Type Parameter when Interpreting Locale Using 'for' Clause



Hi Julian,

> 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"?

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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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