Email Gateway (Aug 19 2022 at 08:01): Email Gateway (Aug 19 2022 at 08:01):From: John Munroe <munddr@gmail.com>
Hi,
If I want to overload a function foo, could I do the following?
typedecl bar
axiomatization
foo :: "'a => int"
where
"foo (x::bar) = 0" and
"foo (x::real) = 1" and
"foo (x::nat) = 2"
I'm feeling that it's at least a sloppy way of overloading. How
different is this compared to the proper way of overloading?
Thanks
John
Email Gateway (Aug 19 2022 at 08:02):From: John Munroe <munddr@gmail.com>
Hi all,
A correction to my question. The code should be:
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 state that foo is ad-hoc polymorphic / overloaded. This is
possible because the assertions are hypothetical, but within L, foo is
ad-hoc / 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: Apr 19 2024 at 01:05 UTC