Email Gateway (Aug 18 2022 at 16:51): Email Gateway (Aug 18 2022 at 16:51):From: Eg Gloor <egglue@gmail.com>
Hello
With the "=" operator, I can do comparisons like:
consts
f :: "'a1 => 'a2"
g :: "'a1 => 'a2 => 'a3"
lemma "f = g"
...
But in HOL.thy, it's defined as
eq :: "['a, 'a] => bool" (infixl "=" 50)
Since Isabelle/HOL is only simply typed with type variables, how come 'a can
be instantiated to 'a1 => 'a2 and 'b can be instantiated to 'a1 => 'a2 =>
'a3, even they are of different arities? However, if f was
f :: "real => real"
then type unification fails with "f = g".
Thx
Email Gateway (Aug 18 2022 at 16:51):From: Eg Gloor <egglue@gmail.com>
On Thu, Jan 27, 2011 at 11:42 AM, Christian Maeder <Christian.Maeder@dfki.de
wrote:
Am 27.01.2011 11:24, schrieb Eg Gloor:
Hello
With the "=" operator, I can do comparisons like:
consts
f :: "'a1 => 'a2"
g :: "'a1 => 'a2 => 'a3"lemma "f = g"
...But in HOL.thy, it's defined as
eq :: "['a, 'a] => bool" (infixl "=" 50)
Since Isabelle/HOL is only simply typed with type variables, how come 'a
can
be instantiated to 'a1 => 'a2 and 'b can be instantiated to 'a1 => 'a2 =>
'a3, even they are of different arities?type variables of polymorphic functions are implicitly quantified and
are instantiated with fresh variables for each occurrence in
applications. Therefore the type of f "'a1 => 'a2" with fresh (aka new)
variables is unified to say "'b1 => 'b2 => 'b3" of g (with "'a2" being
specialized to "b2 => 'b3).Thanks for the reply. 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.
Eg
HTH Christian
However, if f was
f :: "real => real"
then type unification fails with "f = g".
Thx
Email Gateway (Aug 18 2022 at 16:52):From: Christian Maeder <Christian.Maeder@dfki.de>
I'm no Isabelle expert, but I suspect that the types are already
specialized differently. Does "(x::?'a) = (y::?'d)" work?
Cheers Christian
Email Gateway (Aug 18 2022 at 17:04):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 17:11):From: egglue@gmail.com
Thanks for the reply.
Could someone please add to why schematic type variables can't be
specialised? Why don't they behave like type variables?
Thanks
Eg
Email Gateway (Aug 18 2022 at 17:11):From: Eg Gloor <egglue@gmail.com>
On Tue, Feb 1, 2011 at 3:18 PM, Makarius <makarius@sketis.net> wrote:
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.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?
Thanks again
Eg
Makarius
Email Gateway (Aug 18 2022 at 17:11):From: Brian Huffman <brianh@cs.pdx.edu>
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.
Email Gateway (Aug 18 2022 at 17:12):From: Makarius <makarius@sketis.net>
On Thu, 3 Feb 2011, Eg Gloor wrote:
If I understand this correctly, schematic variables can be instantiated
but schematic type variables cannot due to a restriction of
type-inference.
Not quite so. Here is another attempt to summarize the main aspects.
* Term and type variables can be either "arbitrary" (schematic) or
"fixed" (non-schematic, free).
* Schematic term/type variables can be instantiated. For type variables
this effectively means some kind of naive polymorphism.
* Schematic term variables can be explicitly bound via quantification
(!! / \<And>) with arbitrary nesting; type variables cannot be bound
like that.
* Type inference never instantiates schematic term/type variables
written by the user.
* Instead, syntactic type-inference parameters get unified during type
inference, but there is no end-user notation for that (the system
sometimes prints ??'a).
* Goal states with schematic type variables are theoretically OK, but
often break existing proof tools.
Thus, there's no polymorphism of any kind at the meta-level.
The Pure framework indeed lacks proper polymorphism. You only have global
types/consts/theorems that can mention arbitrary types ?'a effectivily
giving you some outermost quantification here. The rest are conjuring
tricks, in the spirit of original Hindley-Milner polymorphism.
Before this is getting more complicated: What is your actual application?
Makarius
Email Gateway (Aug 18 2022 at 17:12):From: Eg Gloor <egglue@gmail.com>
Thanks for the explanation.
- Schematic term/type variables can be instantiated. For type variables
this effectively means some kind of naive polymorphism.I see. But why do you call it naive? If the variables can be instantiated,
then that's polymorphism -- is it not?
Before this is getting more complicated: What is your actual application?
Basically, I'm puzzled by two things:
1) If we look at the following:
axiomatization
func1 :: "nat => nat" and
func2 :: "(nat => nat) => nat" and
func3 :: "'a => 'b => 'c"
where
*: "func2 func1 = 0"
schematic_lemma lem: "EX f (c::?'a). f c = 0"
apply (intro exI)
apply (rule_tac[!] *)
done
thm lem
EX (f::nat => nat) c::nat. f c = (0::nat)
I wasn't expecting c to be of type "nat". Since it uses *, c should be
instantiated to "func1", which is of type "nat => nat". According to the
prf:
protectI % EX f c. f c = 0 %%
(exI % (%x. EX c. x c = 0) % (%a. a) %% (OfClass type_class % TYPE(nat =>
nat)) %% (exI % (%x. x = 0) % func2 func1 %% (OfClass type_class %
TYPE(nat)) ...
f is instantiated to func2 and c is instantiated to func1. How come ?'a is
instantiated to "nat" and not "nat => nat"?
2) For the following:
declare [[unify_search_bound=5]]
ML {*
val p = term_of @{cpat "?f (?c::?'a) = ?v"};
val t = @{term "x (y::nat=>nat) (z::nat=>nat) = (0::nat)"};
val mtchers = Unify.matchers @{theory} [(p,t)] |> Seq.list_of;
pretty_insts @{context} (map (fn x => (x,0)) mtchers)
*}
It returns 3 matchers:
(1) [?c::nat := (x::(nat => nat) => (nat => nat) => nat) (y::nat => nat)
(z::nat => nat), ?f::nat => nat := %a::nat. a, ?v::nat := 0::nat]
[?'a := nat, ?'a1 := nat]
(2) [?c::?'a := ?c::?'a, ?f::?'a => nat := %a::?'a. (x::(nat => nat) => (nat
=> nat) => nat) (y::nat => nat) (z::nat => nat), ?v::nat := 0::nat]
[?'a1 := nat]
(3) [?c::?'a := z::nat => nat, ?f::?'a => ?'a1 := (x::(nat => nat) => (nat
=> nat) => nat) (y::nat => nat), ?v::?'a1 := 0::nat]
[?'a := nat => nat, ?'a1 := nat]
How come "?c" can't be instantiated to "z" but can be instantiated to
"y"? It can do that only if the type of ?c is changed from ?'a to, e.g.,
?'a=>?'b. Since the schematic type variables, e.g., ?'a can be instantiated,
e.g., to "nat" in (1) and to "nat => nat" in (3), why does the type of ?c
need to be explicitly rewritten to, e.g., ?a=>?'b, in order for ?c to be
instantiated to functions like "y" or %x.x? Is this what you mean by "naive
polymorphism"?
Note that even when ?c::?'a=>?'b, there are 2 matchers with ?c := z whereas
there's only 1 matcher with ?c := y. Do you know what's behind
this asymmetry?
Thanks, again, and look forward to your reply!
Eg
Makarius
Email Gateway (Aug 18 2022 at 17:13):From: Lawrence Paulson <lp15@cam.ac.uk>
I've only had time for a brief look at your problem. And I'm not an expert at reading proof objects. But it appears to me that in your first example, the first proof that is found instantiates f to the identity function, so naturally c must be a natural number.
The other point is that unification cannot always be expected to instantiate a type variable to a function type, as the search space would become too large.
Larry Paulson
Email Gateway (Aug 18 2022 at 17:13):From: egglue@gmail.com
On Feb 7, 2011 12:25pm, Lawrence Paulson <lp15@cam.ac.uk> wrote:
I've only had time for a brief look at your problem. And I'm not an
expert at reading proof objects. But it appears to me that in your first
example, the first proof that is found instantiates f to the identity
function, so naturally c must be a natural number.
Thanks. I should note that the schematic_lemma lem: "EX f (c::?'a). fc =
(0::nat)", but the proof object is right. I think you're right -- f is
instantiated to the identity function. If I explicitly instantiate each
variable explicitly, I get the right type.
The other point is that unification cannot always be expected to
instantiate a type variable to a function type, as the search space would
become too large.
Is this a limitation of the logic or is it a restriction intended by the
implementation? Do you know in what circumstances does the unification not
instantiate a type variable to a function type?
Thanks
Eg
Larry Paulson
On 5 Feb 2011, at 01:22, Eg Gloor wrote:
Thanks for the explanation.
>
>
- Schematic term/type variables can be instantiated. For type variables
this effectively means some kind of naive polymorphism.
>
>
I see. But why do you call it naive? If the variables can be
instantiated,
then that's polymorphism -- is it not?
>
>
>
Before this is getting more complicated: What is your actual
application?
>
>
Basically, I'm puzzled by two things:
>
1) If we look at the following:
>
axiomatization
func1 :: "nat => nat" and
func2 :: "(nat => nat) => nat" and
func3 :: "'a => 'b => 'c"
where
*: "func2 func1 = 0"
>
schematic_lemma lem: "EX f (c::?'a). fc = 0"
apply (intro exI)
apply (rule_tac[!] *)
done
>
thm lem
>
EX (f::nat => nat) c::nat. fc = (0::nat)
>
I wasn't expecting c to be of type "nat". Since it uses *, c should be
instantiated to "func1", which is of type "nat => nat". According to the
prf:
>
protectI % EX f c. fc = 0 %%
(exI % (%x. EX c. xc = 0) % (%a. a) %% (OfClass type_class % TYPE(nat =>
nat)) %% (exI % (%x. x = 0) % func2 func1 %% (OfClass type_class %
TYPE(nat)) ...
>
f is instantiated to func2 and c is instantiated to func1. How come ?'a
is
instantiated to "nat" and not "nat => nat"?
>
2) For the following:
>
declare [[unify_search_bound=5]]
>
ML {*
val p = term_of @{cpat "?f (?c::?'a) = ?v"};
val t = @{term "x (y::nat=>nat) (z::nat=>nat) = (0::nat)"};
val mtchers = Unify.matchers @{theory} [(p,t)] |> Seq.list_of;
pretty_insts @{context} (map (fn x => (x,0)) mtchers)
*}
>
It returns 3 matchers:
(1) [?c::nat := (x::(nat => nat) => (nat => nat) => nat) (y::nat => nat)
(z::nat => nat), ?f::nat => nat := %a::nat. a, ?v::nat := 0::nat]
>
[?'a := nat, ?'a1 := nat]
>
(2) [?c::?'a := ?c::?'a, ?f::?'a => nat := %a::?'a. (x::(nat => nat)
=> (nat
=> nat) => nat) (y::nat => nat) (z::nat => nat), ?v::nat := 0::nat]
>
[?'a1 := nat]
>
(3) [?c::?'a := z::nat => nat, ?f::?'a => ?'a1 := (x::(nat => nat) =>
(nat
=> nat) => nat) (y::nat => nat), ?v::?'a1 := 0::nat]
>
[?'a := nat => nat, ?'a1 := nat]
>
How come "?c" can't be instantiated to "z" but can be instantiated to
"y"? It can do that only if the type of ?c is changed from ?'a to, eg,
?'a=>?'b. Since the schematic type variables, eg, ?'a can be
instantiated,
eg, to "nat" in (1) and to "nat => nat" in (3), why does the type of ?c
need to be explicitly rewritten to, eg, ?a=>?'b, in order for ?c to be
instantiated to functions like "y" or %xx? Is this what you mean
by "naive
polymorphism"?
>
Note that even when ?c::?'a=>?'b, there are 2 matchers with ?c := z
whereas
there's only 1 matcher with ?c := y. Do you know what's behind
this asymmetry?
>
Thanks, again, and look forward to your reply!
>
Eg
>
>
Makarius
>
Email Gateway (Aug 18 2022 at 17:13):From: Lawrence Paulson <lp15@cam.ac.uk>
It isn't imposed by the logic, but it is more or less essential in any practical implementation.
Your example (with a function variable) hits the most difficult aspect of higher-order unification, namely, the creation of possible functions to solve a constraint involving a function variable. The restriction prevents transforming a variable of type ?'a into one of some function type.
Larry Paulson
Last updated: Apr 26 2024 at 20:16 UTC