[isabelle] Uses of type quantification


Brian Huffman, Peter White, and I are interested in having a limited form of type quantification added to Isabelle/HOLCF. It turns out that many of Haskell's constructor classes (most notably functors and monads) are associated with axioms that require quantifying over type variables. For example, one of the axioms of the monad class is the Left unit law. It states that for any monad instance 'm, containing methods for unit and bind with the following polymorphic signatures:

  unit :: "'a -> 'a $ 'm"
  bind :: "'a $ 'm -> ('a -> 'b $ 'm) -> 'b $ 'm",

(the infix ($) operator is a binary type constructor that we use to simulate constructor classes in Isabelle/HOLCF). Then the following "left unit" axiom holds for the monad instance:

  "ALL_TY 'a. bind $ (unit $ (x::'a)) $ f = f $ x".

Note that the outermost "ALL_TY" operator is quantifying over types, not terms. However, the result is still a Boolean term, not a new type. Tom Melham worked out a consistent extension to higher order logic that incorporates this operator [1]. Without this quantifier, then the axiom for the monad class would have two type variables, which is disallowed by Isabelle's axclass mechanism. Even if the axclass package allowed multi-parameter type classes, the axioms become much more cumbersome to state and use without type quantification.

We are wondering what other applications people have where this type-quantification operator would be useful, either in Isabelle or other implementations of classical higher order logic?


[1]: T. F. Melham, "The HOL Logic Extended with Quantification over Type Variables", Formal Methods in System Design, vol. 3, nos. 1-2 (August 1993), pp. 7-24.

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