Re: [isabelle] Uses of type quantification

Hello John,

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 complicated.

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 [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?


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