# [isabelle] Uses of type quantification

Hello,

`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?
`
Thanks,
-john

`[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.*