Re: [isabelle] Comparing polymorphic functions
- To: Eg Gloor <egglue at gmail.com>
- Subject: Re: [isabelle] Comparing polymorphic functions
- From: Makarius <makarius at sketis.net>
- Date: Tue, 1 Feb 2011 16:18:11 +0100 (CET)
- Cc: cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <AANLkTi=2yDP7JNzG-tJHJE7JOXybL5YWiQEnCKkrWLUfirstname.lastname@example.org>
- References: <AANLkTik_QPi0HNJ9WShk7s_nc9jsbwH7_X9H6a-UDjaemail@example.com> <4D415A30.firstname.lastname@example.org> <AANLkTi=2yDP7JNzG-tJHJE7JOXybL5YWiQEnCKkrWLUemail@example.com>
- User-agent: Alpine 1.10 (LNX 962 2008-03-14)
On Thu, 27 Jan 2011, Eg Gloor wrote:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and