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.

Cheers,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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