Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unexpected(?) behaviour of polymorphic constants

Email Gateway (Mar 01 2024 at 15:34):

From: Mike Stannett <cl-isabelle-users@lists.cam.ac.uk>
We've been looking at the behaviour of polymorphic constants, and have
derived something that seems a bit anomalous. The following proof,
involving a polymorphic constant called polyval, shows that

"polyval = (0::nat) ∧ polyval = (True::bool)"

which seems to say that polyval is two different constants, of different
types, at the same time. Is this intended?, i.e. does the declaration of
polyval as a polymorphic constant mean "polyval is a constant whose type is
as yet undetermined" or "each type is declared to contain its own constant
called polyval"?

fun demo :: "nat ⇒ bool ⇒ nat"
where "demo x y = (if y then x + 1 else 0)"

consts polyval :: "'a"

abbreviation polyresult :: "nat"
where "polyresult ≡ demo (polyval :: nat) (polyval :: bool)"

lemma michael:
assumes "polyresult = 1"
shows "polyval = (True::bool)"
by (metis assms demo.elims zero_neq_one)

lemma mps:
assumes "polyresult = 1"
shows "polyval = (0 :: nat)"
using assms michael by fastforce

lemma unexpected:
assumes "polyresult = 1"
shows "polyval = (0::nat) ∧ polyval = (True::bool)"
proof -
have lhs: "polyval = (0::nat)" using assms mps by blast
have rhs: "polyval = (True::bool)" using assms michael by blast
show ?thesis using lhs rhs by blast
qed

Regards, Michael Foster/Mike Stannett

Email Gateway (Mar 01 2024 at 17:40):

From: Peter Lammich <lammich@in.tum.de>
That's the expected behavior of Isabelle's top-level polymorphism: the
polymorphic types can be instantiated to whatever (sort-compatible) type.

Note however, that this does not hold for fixed/bound variables, e.g. in

"let polyval::'a = undefined in  (polyval::nat) < 5"

you get a type-error, as 'a is not equal to nat.

Email Gateway (Mar 02 2024 at 13:37):

From: Lawrence Paulson <lp15@cam.ac.uk>
This is how overloading works. Your ability to write x+y without knowing whether + refers to addition on natural numbers, integers, rationals, reals, complex numbers, quaternions, etc, hinges on it.

And thanks to the axiomatic type class system, things are organised such that innumerable arithmetic laws are made available to all types satisfying the necessary underlying axioms. And similarly for overloading in other domains.

Larry Paulson

Last updated: Apr 29 2024 at 04:18 UTC