*To*: Tom Ridge <Thomas.Ridge at cl.cam.ac.uk>*Subject*: Re: [isabelle] Uses of type quantification*From*: John Matthews <matthews at galois.com>*Date*: Wed, 7 Sep 2005 17:26:30 -0700*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <431EACCC.4080702@cl.cam.ac.uk>*References*: <817439747567edb58bbd67d41ed34f6c@galois.com> <431EACCC.4080702@cl.cam.ac.uk>

Hi Tom,

-john On Sep 7, 2005, at 2:03 AM, Tom Ridge wrote:

Hello John,I am currently in the process of adding type quantification to HOLLight, although I wouldn't expect to finish anytime soon. As you canprobably imagine, things like alpha conversion are slightly morecomplicated.I would guess it would be quite a lot of work to add to Isabelle, butperhaps others can provide more information.There are lots of uses for type quantification. I have one example at http://homepages.inf.ed.ac.uk/s0128214/doc/typeQuantification.pdf but I don't think it is a particularly good one.There was some discussion by Rob Arthan and others on this topic onthe HOL list, and this is probably the best place to look. Variouspeople (e.g. Harrison, in - I think -@INPROCEEDINGS{harrison-model, crossref = "hol98", author = "John Harrison", title = "Formalizing Basic First Order Model Theory", pages = "153--170"} @PROCEEDINGS{hol98, 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 themby related assumptions. FOL is a closed system. HOL is open, because Ican assert an axiom "forall x:'a. I x = x", and via typeinstantiation, I can get "forall x:'b. I x = x" for any 'b. Thecorresponding assumption is "forall 'a. forall x:'a. I x = x", but ofcourse, this can't be expressed currently. The reason I want to dothis is another story.I would also imagine that it is possible to do without typequantification in many areas, and this may be the case with yourexample. For example, you could just assert the axiombind $ (unit $ (x::'a)) $ f = f $ xbut then you would not get the safety of the axclass mechanism, andwould have to manually track definitions of unit and bind to make surethey satisfied this axiom.Cheers Tom John Matthews wrote:Hello,Brian Huffman, Peter White, and I are interested in having a limitedform of type quantification added to Isabelle/HOLCF. It turns outthat many of Haskell's constructor classes (most notably functors andmonads) are associated with axioms that require quantifying over typevariables. For example, one of the axioms of the monad class is theLeft unit law. It states that for any monad instance 'm, containingmethods 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 tosimulate 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 newtype. Tom Melham worked out a consistent extension to higher orderlogic 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 theaxclass package allowed multi-parameter type classes, the axiomsbecome much more cumbersome to state and use without typequantification.We are wondering what other applications people have where thistype-quantification operator would be useful, either in Isabelle orother implementations of classical higher order logic?Thanks, -john[1]: T. F. Melham, "The HOL Logic Extended with Quantification overType Variables",Formal Methods in System Design, vol. 3, nos. 1-2 (August 1993),pp. 7-24.

**Follow-Ups**:**Re: [isabelle] Uses of type quantification***From:*Konrad Slind

**References**:**[isabelle] Uses of type quantification***From:*John Matthews

**Re: [isabelle] Uses of type quantification***From:*Tom Ridge

- Previous by Date: Re: [isabelle] Uses of type quantification
- Next by Date: Re: [isabelle] Uses of type quantification
- Previous by Thread: Re: [isabelle] Uses of type quantification
- Next by Thread: Re: [isabelle] Uses of type quantification
- Cl-isabelle-users September 2005 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list