Re: [isabelle] Uses of type quantification
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 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