Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Ad-hoc vs. parametrically polymorphic


view this post on Zulip Email Gateway (Aug 19 2022 at 08:27):

From: John Munroe <munddr@gmail.com>
Hi

I have a question about overloading. Suppose I have the following

axiomatization
foo :: "'a => int"

locale L =
assumes
ax1 : "foo(x::nat) = 0" and
ax2 : "foo(x::int) = 1" and
ax3 : "foo(x::real) = 2"

Please correct or confirm my understanding of this: foo is declared as
being a parametrically polymorphic predicate, but the axioms in the
locale L force foo to be ad-hoc polymorphic / overloaded. This is
possible because the assertions in a locale are hypothetical (since
they're axioms), but within L, foo is ad-hoc polymorphic / overloaded
rather than parametrically polymorphic.

So is defining foo as a method of a type class the best way to
overload foo? AFAIK type classes don't exactly implement ad-hoc
polymorphism. For instance, type classes are shown up as types and a
type class does not need to explicitly state its behaviour for each
type, because a type class could extend another type class. My
understanding of ad-hoc polymorphism / overloading is that the way a
function behaves must be explicitly defined for each type.

Thanks

John


Last updated: Mar 28 2024 at 08:18 UTC