Email Gateway (Aug 18 2022 at 18:31): Email Gateway (Aug 18 2022 at 18:31):From: John Munroe <munddr@gmail.com>
Hi,
If I have the following:
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?
Any input will be appreciated. Thanks.
John
Email Gateway (Aug 18 2022 at 18:31):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi John,
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
signature.asc
Last updated: Apr 26 2024 at 04:17 UTC