Email Gateway (Aug 18 2022 at 17:18): Email Gateway (Aug 18 2022 at 17:18):From: Eg Gloor <egglue@gmail.com>
On Wed, Mar 30, 2011 at 9:01 PM, Makarius <makarius@sketis.net> wrote:
On Wed, 30 Mar 2011, egglue@gmail.com wrote:
axiomatization
f :: "'a => 'b" and
g :: "nat => nat" where
ax : "f = g"
Why are 'a and 'b fixed under "axiomatization"?
The specification is considered as one logical unit, where f and g are
always the same local entity, with fixed types. The context is essentially
this:fix_type 'a and 'b -- "implicit"
fix g :: "'a => 'b" and g :: "nat => nat"
assume ax : "f = g"Later the types become arbitrary in the result, so the consts f and g in
the target context can be used at different type.It is always the same game. This is how naive polymorphism works. There
is no type quantification. (It would make the logic very complicated, or
break down).I see. So Isabelle/HOL isn't truly polymorphic since there isn't type
quantification. Could you provide some pointers to material explaining the
naive polymorphism?
Thanks
Eg
It seems that I can produce very much the same declaration with:
axiomatization
f:: "'a => 'b" and
g :: "nat => nat"axioms
ax : "f = g"Why is f polymorphic in "axioms" but not in "axiomatization"?
'axioms' is an obsolete form, better do it like this:
axiomatization
f :: "'a => 'b" and
g :: "nat => nat"axiomatization where
ax : "f = g"Separate specifications have separate scopes wrt. polymorphism. The consts
axiomatized in the first one can be used at different types at the second
one.Makarius
Email Gateway (Aug 18 2022 at 17:19):From: Makarius <makarius@sketis.net>
You can probably find a lot of references just by searching through the
archives of the isabelle-users mailing list -- this is a recurrent topic.
Just one arbitray paper where the topic is also mentioned
http://www4.in.tum.de/~wenzelm/papers/local-theory.pdf -- it is about
giving an impression of Hindley-Milner polymorphism in a system with plain
schematic types only.
Makarius
Email Gateway (Aug 18 2022 at 17:27):From: Eg Gloor <egglue@gmail.com>
Hello all,
Does anyone know why the following gives an error saying: "Coercion
inference failed: weak unification of subtype constraints fails"?
axiomatization
f :: "'a => 'b" and
g :: "nat => nat" where
ax : "f = g"
However,
lemma "f = g"
successfully goes through without giving an error.
Any help will be appreciated.
Eg
Email Gateway (Aug 18 2022 at 17:28):From: Makarius <makarius@sketis.net>
On Wed, 30 Mar 2011, Eg Gloor wrote:
axiomatization
f :: "'a => 'b" and
g :: "nat => nat" where
ax : "f = g"
Here 'a and 'b are fixed in the scope where "f = g" needs to type check.
axiomatization
f :: "'a => 'b" and
g :: "nat => nat" where
lemma "f = g"
Here f is polymorphic and can be instantiated to "nat => nat".
Makarius
Email Gateway (Aug 18 2022 at 17:28):From: egglue@gmail.com
I see. Why are 'a and 'b fixed under "axiomatization"? It seems that I can
produce very much the same declaration with:
axiomatization
f:: "'a => 'b" and
g :: "nat => nat"
axioms
ax : "f = g"
Why is f polymorphic in "axioms" but not in "axiomatization"?
Thanks
Eg
Email Gateway (Aug 18 2022 at 17:28):From: Makarius <makarius@sketis.net>
On Wed, 30 Mar 2011, egglue@gmail.com wrote:
axiomatization
f :: "'a => 'b" and
g :: "nat => nat" where
ax : "f = g"
Why are 'a and 'b fixed under "axiomatization"?
The specification is considered as one logical unit, where f and g are
always the same local entity, with fixed types. The context is
essentially this:
fix_type 'a and 'b -- "implicit"
fix g :: "'a => 'b" and g :: "nat => nat"
assume ax : "f = g"
Later the types become arbitrary in the result, so the consts f and g in
the target context can be used at different type.
It is always the same game. This is how naive polymorphism works. There
is no type quantification. (It would make the logic very complicated, or
break down).
It seems that I can
produce very much the same declaration with:axiomatization
f:: "'a => 'b" and
g :: "nat => nat"axioms
ax : "f = g"Why is f polymorphic in "axioms" but not in "axiomatization"?
'axioms' is an obsolete form, better do it like this:
axiomatization
f :: "'a => 'b" and
g :: "nat => nat"
axiomatization where
ax : "f = g"
Separate specifications have separate scopes wrt. polymorphism. The
consts axiomatized in the first one can be used at different types at the
second one.
Makarius
Last updated: Apr 20 2024 at 12:26 UTC