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 http://www4.in.tum.de/~wenzelm/papers/axclass-TPHOLs97.pdf

The more recent papers by Haftmann and Wenzel on "Constructive Type Classes" http://www4.in.tum.de/~wenzelm/papers/constructive_classes.pdf and "Local theory specifications in Isabelle/Isar" http://www4.in.tum.de/~wenzelm/papers/constructive_classes.pdf explain 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.


	Makarius




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