Re: [isabelle] Uses of type quantification
FWIW, I implemented type quantification for HOL90 about 10 years ago.
made it into public release. Tom Melham still has the code, if you're
Michael Norrish and I occasionally think about adding this back into
"experimental kernel" that he's developed for HOL-4.
Also, there was a recent thread about this sort of thing on the
in April of this year,
(above path needs to have the carriage-return removed)
sparked by my student's realization that a natural definition of the
can't be made without type quantification. Recall that the regular sets
that are recognized by a DFA. So
Regular (L) <=> ?M. DFA(M) /\ !w. w \in L <=> M accepts w
On the lhs, the type of Regular is ('a -> bool) -> bool. But a general
definition of DFA would be polymorphic in the state type and the
type of string elements (treating strings as 'a lists, say). Being able
type quantify the state type on the rhs of the definition would help
as pointed out in the ensuing discussion, it isn't actually crucial.
On Sep 7, 2005, at 6:26 PM, John Matthews wrote:
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
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
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), pp. 7-24.
This archive was generated by a fusion of
Pipermail (Mailman edition) and