Re: [isabelle] Comparing polymorphic functions



On Thu, Feb 3, 2011 at 10:49 AM, Eg Gloor <egglue at gmail.com> wrote:
> If I understand this correctly, schematic variables can be instantiated but
> schematic *type* variables cannot due to a restriction of type-inference.
> Thus, there's no polymorphism of any kind at the meta-level. Likewise, with
> type variables because they are free variables. So it's expected that this
> wouldn't work:
>
> lemma "(x::'a) = (y::'b)"
>
> Because both 'a and 'b are free variables. But this works fine:
>
> const
> x :: 'a
>
> lemma "x = (y::'b)"
>
> Isn't 'a regarded as a free variable? How come it can be instantiated?

One way to interpret a top-level declaration like "const x :: 'a",
whose type has a free type variable, is that it actually declares an
infinite family of top-level constants. In this case, you get an
infinite number of different constants, all named "x", but each with a
different type.

Later, when you state a lemma like "x = (y::'b)", type inference must
select which one of this family of constants named "x" you mean: Here,
it concludes that you must have meant "x::'b", since that is the only
one that makes the lemma type-correct.

- Brian





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