*To*: John Matthews <matthews at galois.com>*Subject*: Re: [isabelle] Uses of type quantification*From*: Tom Ridge <Thomas.Ridge at cl.cam.ac.uk>*Date*: Wed, 07 Sep 2005 10:03:08 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <817439747567edb58bbd67d41ed34f6c@galois.com>*References*: <817439747567edb58bbd67d41ed34f6c@galois.com>*User-agent*: Mozilla Thunderbird 0.8 (X11/20040913)

Hello John,

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.

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

bind $ (unit $ (x::'a)) $ f = f $ x

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 out thatmany 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 unitand 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, notterms. However, the result is still a Boolean term, not a new type. TomMelham worked out a consistent extension to higher order logic thatincorporates this operator [1]. Without this quantifier, then the axiomfor the monad class would have two type variables, which is disallowedby Isabelle's axclass mechanism. Even if the axclass package allowedmulti-parameter type classes, the axioms become much more cumbersome tostate and use without type quantification.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 over TypeVariables",Formal Methods in System Design, vol. 3, nos. 1-2 (August 1993),pp. 7-24.

**Follow-Ups**:**Re: [isabelle] Uses of type quantification***From:*John Matthews

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

- Previous by Date: [isabelle] DATE 2006 paper submission deadline very soon
- 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