Re: [isabelle] Is this overloading?



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

On Mon, Jul 30, 2012 at 12:45 AM, John Munroe <munddr at gmail.com> wrote:
> 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





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