Re: [isabelle] Uses of type quantification
I have put up a definition of alpha equivalence for HOL terms involving type
which may be of interest.
John Matthews wrote:
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 Type
Formal Methods in System Design, vol. 3, nos. 1-2 (August 1993),
This archive was generated by a fusion of
Pipermail (Mailman edition) and