Re: [isabelle] Polymorphism and type class

Hi John,

> typedecl A
> typedecl B
> axiomatization
> f :: "'a => nat"
> axioms
> ax1 : "f (x::A) = 0"
> ax2 : "f (x::B) = 1"
> Is the mechanism for "inspecting" the type of the argument of f
> essentially defining a type class, or is it something else? If it's
> indeed something else, then why isn't a type class used instead?

logically, equational theorems are just »rules« with a certain typing,
and this typing »decides« which »rules« actually can be applied to a
redex.  This does not need any special mechanisms since the logic is not
a programming language: all types are present at all time.

Another story is how constants can be *defined* overloaded.  The
end-user mechanism used mostly nowadays are indeed type classes similar
to Haskell, but on the foundational level this manifests as a special
discipline of admissible overloaded definition – ask if you want to know
more on that.




PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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