[isabelle] Type classes vs. locales?



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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.