Email Gateway (Aug 19 2022 at 15:36): Email Gateway (Aug 19 2022 at 15:36):From: Holden Lee <hl422@cam.ac.uk>
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
Email Gateway (Aug 19 2022 at 15:36):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Holden,
In your situation of abstract algebra, locales are better than type classes, as you want
to talk about carriers, sub-structures, and existence of structures. However, some of your
comments need some refinement.
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).
This is not correct. You can define a type ('a, 'b) prod_ring (e.g., via typedef) and do
an instance declaration for ring:
instantiation prod_ring (ring, ring) ring begin
(* definition of ring operations on product *)
instance (* proof *)
end
This declaration is valid for any two types with the ring structure without saying which
ring they are.
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..."
You can phrase a statement like "for every prime p, there exists a field F_p with p
elements" on the type level as follows. Define prime :: "nat => nat" as the distinct
enumeration of all the primes, e.g., prime n is the n-th prime. Then, define a type 'a F_p
as a type that contains prime CARD('a) elements. Then, you can do
instantiation F_p (finite) field begin
Since Isabelle has types with exactly n elements for any natural number n > 0, you get
what you want. But I admit that this is a bit cumbersome.
For completeness, there are a few cases where type classes are superior to locales.
Code generation within locales with assumptions essentially does not work. You can only
generate code for interpretations for which you have to manually redefine the constants
introduced in the locale. With type classes, the code generator takes care of overloaded
operations.
Overloading of polymorphic operations. If an overloaded operation (like addition in a
ring) occurs with multiple different instances, the locale approach requires you to use a
different constant for each instance. In that case, you normally have to introduce a
locale that combines multiple instances, too. Here's an example with type classes:
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
Email Gateway (Aug 19 2022 at 15:36):From: Gottfried Barrow <igbi@gmx.com>
I don't know all the details about how to overload notation, but it
appears that overloading notation through type classes is generally
superior to doing it other ways, and notation can be of huge importance.
If you use type classes, you obtain other magic by default, in
particular with the code generator, which at a minimum comes into play
with the "value" command. It's very useful to always be able to do some
experimental computations with "value", and very annoying when "value"
won't work for my functions, even though my logic is good.
Regards,
GB
Last updated: Apr 24 2024 at 04:17 UTC