*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 18:47:10 +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)

http://homepages.inf.ed.ac.uk/s0128214/ which may be of interest. T 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.

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

- 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