Re: [isabelle] Uses of type quantification
Thanks for the pointers. I'm glad to hear you find type quantification
to be useful enough to add it to HOL light! I'll see if I can dig up
the type quantification thread on info-hol.
On Sep 7, 2005, at 2:03 AM, Tom Ridge wrote:
I am currently in the process of adding type quantification to HOL
Light, although I wouldn't expect to finish anytime soon. As you can
probably imagine, things like alpha conversion are slightly more
I would guess it would be quite a lot of work to add to Isabelle, but
perhaps others can provide more information.
There are lots of uses for type quantification. I have one example at
but I don't think it is a particularly good one.
There was some discussion by Rob Arthan and others on this topic on
the HOL list, and this is probably the best place to look. Various
people (e.g. Harrison, in - I think -
crossref = "hol98",
author = "John Harrison",
title = "Formalizing Basic First Order Model Theory",
pages = "153--170"}
editor = "Jim Grundy and Malcolm Newey",
booktitle = "Theorem Proving in Higher Order Logics:
11th International Conference, TPHOLs'98",
series = "Lecture Notes in Computer Science",
volume = 1497,
address = "Canberra, Australia",
date = "September/October 1998",
year = 1998,
publisher = "Springer-Verlag"}
) mention it in various contexts.
My own reasons for adding it are so that HOL becomes a closed system,
in the sense that one can remove instances of axioms and replace them
by related assumptions. FOL is a closed system. HOL is open, because I
can assert an axiom "forall x:'a. I x = x", and via type
instantiation, I can get "forall x:'b. I x = x" for any 'b. The
corresponding assumption is "forall 'a. forall x:'a. I x = x", but of
course, this can't be expressed currently. The reason I want to do
this is another story.
I would also imagine that it is possible to do without type
quantification in many areas, and this may be the case with your
example. For example, you could just assert the axiom
bind $ (unit $ (x::'a)) $ f = f $ x
but then you would not get the safety of the axclass mechanism, and
would have to manually track definitions of unit and bind to make sure
they satisfied this axiom.
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
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