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 "" would be "% f. f 0" :: "('a =>
> 'b) => 'b". Instead, it is "% type f. 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

The phantom parameter you experience will vanish immediately if the 'a
parameter is instantiated to a fixed type.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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