[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 . 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?
: T. F. Melham, "The HOL Logic Extended with Quantification over
Formal Methods in System Design, vol. 3, nos. 1-2 (August 1993),
This archive was generated by a fusion of
Pipermail (Mailman edition) and