Re: [isabelle] Uses of type quantification



Hi Jeremy,

An alternative way of handling this situation would be to actually have
constructor classes, as a generalisation of the present type class mechanism.

This is a good opportunity to give a shameless plug for the paper that motivated our wish for type quantification in Isabelle :)

  "Axiomatic Constructor Classes in Isabelle/HOLCF"
  Brian Huffman, John Matthews, and Peter White
  TPHOLs 2005

The aim of the paper is to enable Haskell-style constructor classes in HOLCF, plus class axioms that all class instances must obey. It turns out that we can simulate constructor classes relatively cleanly in HOLCF.

We can also simulate type quantification in this setting, but it is a more cumbersome process. Essentially we have to specify any given type-quantified class axiom A instead in terms of an untyped axiom A', that quantifies over a universal domain. We then use a projection-embedding pair to "lift" A' to A. We can use A to prove generic theorems about the class, but we must use the untyped A' axiom when admitting a new instance of the class. Type quantification would eliminate this detour.

Cheers,
-john






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