*To*: Holden Lee <hl422 at cam.ac.uk>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Type classes vs. locales?*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 26 Aug 2014 15:56:24 +0200*In-reply-to*: <CAKSvo_ZewXUvi+JVoPa78GVunzrGJebn0bL7ucHJGXx+aVSE9g@mail.gmail.com>*References*: <CAKSvo_ZewXUvi+JVoPa78GVunzrGJebn0bL7ucHJGXx+aVSE9g@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.0

Dear Holden,

> 2. Anything involving types that depend on 2+ types cannot be expressed > using typeclasses (ex. (a)-(b), a product of 2 arbitrary rings cannot be > interpreted as a type of class ring, "arbitrary" meaning I haven't chosen a > specific instance).

instantiation prod_ring (ring, ring) ring begin (* definition of ring operations on product *) instance (* proof *) end

> 4. However, there is no automated way to construct instances of > typeclasses (creating classes is allowed only at top-level, so there is no > dependence on parameters) or talk about their existence. Using a typeclass > representing finite fields, you can't say "for every prime p, there exists > a field F_p with p elements," you can only say "given a finite field with p > elements..."

instantiation F_p (finite) field begin

For completeness, there are a few cases where type classes are superior to locales.

lemma fixes f :: "'a :: ring => 'b :: ring => 'c :: ring" assumes "!!a b c d. f (a + b) (c + d) = f a c + f b d" shows "..." Best, Andreas On 26/08/14 15:24, Holden Lee wrote:

In Isabelle, (A) what can be done using locales that can't be done using typeclasses, and (B) what can be done using locales that would be inconvenient with typeclasses? I've read about both of them, but am still trying to find a clear-cut answer, and hoping some discussion will clarify things. Here are some of my thoughts, which might or might not be correct, so comment and add your own thoughts. I'm mostly interested in constructions from abstract algebra. Here are some examples to draw on: (a) ring homomorphism, (b) the product of 2 arbitrary rings, (c) the polynomial algebra R[X_1,...,X_n] over R, (d) the finite fields F_p, (e) the localization S^{-1}R (a ring constructed from R and a multiplicative subset S of R, or any subset, if you prefer), combinations and reinterpretations of these (ex. the vector space F_p[X_1,...,X_n] over F_p) 1. In general, locales are more powerful, but lack the automatic type-checking that types give. 2. Anything involving types that depend on 2+ types cannot be expressed using typeclasses (ex. (a)-(b), a product of 2 arbitrary rings cannot be interpreted as a type of class ring, "arbitrary" meaning I haven't chosen a specific instance). Anything depending on 1 type can be expressed using typeclasses, if the representation has to be done using typeclasses every step of the way. Are there more theoretical restrictions? 3. You can't use a parameter to construct a type (ex. finite field F_p). (i) Using locales, this isn't a problem because you can certainly construct a ring_scheme, etc. from a parameter, using an ordinary function. (ii) Using typeclasses, you would have to "bake in" a parameter, for instance have a function card_Fp::'a=>nat discarding the input of type 'a and just giving the cardinality of the field (actually here you can sidestep this and just return the CARD of 'a, but you can't do this in general, like recovering S in (e)). 4. However, there is no automated way to construct instances of typeclasses (creating classes is allowed only at top-level, so there is no dependence on parameters) or talk about their existence. Using a typeclass representing finite fields, you can't say "for every prime p, there exists a field F_p with p elements," you can only say "given a finite field with p elements..." This is mathematically a bit odd because you hypothesize everything you need about the type you want (ex. finite fields) as assumptions in the class (including everything necessary to recover the original input data), whereas in the locale case you can construct it first, and then prove that it satisfies the assumptions you want. 5. A result proven with locales can always be converted to the equivalent result with typeclasses by interpretation. However, a result proved with typeclasses cannot be converted to locales, because instantiation of a typeclass is not allowed inside a proof. -Holden

**References**:**[isabelle] Type classes vs. locales?***From:*Holden Lee

- Previous by Date: [isabelle] Type classes vs. locales?
- Next by Date: Re: [isabelle] RC4: sledgehammer on Cygwin crashed once; temp file not removed
- Previous by Thread: [isabelle] Type classes vs. locales?
- Next by Thread: Re: [isabelle] Type classes vs. locales?
- Cl-isabelle-users August 2014 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