Re: [isabelle] Questions about theories distributed with Isabelle
On Sat, 27 Jul 2013, Josh Tilles wrote:
Does the Isabelle community at large believe that "axiomatic type
classes" cannot be "first-class citizens of the logic"? If so, I'd be
interested to know *why* that's the case, but it's not required so don't
spend too much time explaining.
There are indeed some funny believes about certain aspects of Simple Type
Theory (Isabelle Pure and HOL), leading to Isabelle insider jokes like
"axiomatic type classes are definitional" and "HOL typedef is axiomatic".
(The second one is off-topic here.)
My master's thesis from 1994 demonstrates how type classes are made
first-class citizens of Isabelle/Pure in most respects; this was later
published on TPHOLs 1997, see also
The more recent papers by Haftmann and Wenzel on "Constructive Type
and "Local theory specifications in Isabelle/Isar"
further how everything fits together: type classes, locales, definitional
specifications within any such "module system".
This is all very close to the actual logic, but as usual in Isabelle, the
logic alone only serves fountational purposes. Extra-logical add-ons like
code generation are just as important. For end-users it hardly matters
what is the core logic and what not, as long as it works in symphony.
This archive was generated by a fusion of
Pipermail (Mailman edition) and