Re: [isabelle] Comparing polymorphic functions



On Thu, 27 Jan 2011, Eg Gloor wrote:

consts
f :: "'a1 => 'a2"
g :: "'a1 => 'a2 => 'a3"

So it seems like it isn't simply-typed afterall, since "'a2" can be specialised to "'b2 => 'b3". Or is that limited to type variables? If I do something similar with schematic types:

schematic_lemma test: "(x::?'a=>?'b=>?'c) = (y::?'d=>?'e)"

I get a type unification error there. It seems ?'e can't be specialised to "?'b => ?'c" in this case.

For the logical framework, schematic variables are arbitrary (can be instantiated), while free variables are fixed (local constant that might become arbitrary after leaving the scope).

Type inference has a third category of "parameters" that can get unified in the type checking process. There is no user notation for that, apart from nameless dummies "_". Otherwise type-inference insists that schematic and free variables work out as they are written, no instantiation of schematic variables here.

The above 'schematic_lemma' would give you a chance to instantiate schematic variables in the course of reasoning, after type-checking has already succeeded. Further confusion might be causes by proof tools that choke on schematic type variables in a goal.


	Makarius





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