[isabelle] Ad-hoc vs. parametrically polymorphic


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

foo :: "'a => int"

locale L =
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.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.