Type classes versus locales
[Isabelle locales type classes As we’ve seen in an earlier post, type classes are a convenient mechanism for managing the overloading of syntax in a principled manner: types share syntax and related properties. For example, the familiar arithmetic operators share commutative, distributive and associative laws on numeric types as different as the integers and the complex numbers. We also saw how to introduce a new type (of quaternions) and quickly bring it “into the fold” of arithmetic types through a few instance declarations. The main limitation of type classes is that the syntax and properties are associated with a type, exactly one type, and in only one way. Locales manage syntax and axioms in a more general way, e.g. to deal with abstract algebra.
The problem of multiple type class instantiations
For an example of “only one way”, consider the various ways to order lists, based on an ordering of their elements. (Think of strings over an alphabet.) There is the usual lexicographic ordering where $b > ab > aab > \cdots$, or the version where the length of the string dominates (so now $b < ab$). Both are total orderings and they are incompatible, so it is impossible for a single development to involve both. Similarly, sets are ordered by the subset relation, from which they inherit the distributed lattice of unions and intersections. But we often want to use other orderings with sets.
The big problem, as mentioned earlier, is that type classes only constrain types. That makes them useless for things that are not types, such as groups. Locales solve this problem, so what are they?
Locales: the basics
I ought to know everything about locales, because I was there at the beginning (as the PhD supervisor of Florian Kammüller). And yet a guy who knew everything about the Model T may not be able to explain the workings of a Tesla, due like so much to Makarius Wenzel. The main point is that, logically, locales are nothing more than predicate symbols. Their magic comes from special support in Isabelle for declaring and using them, managing their associated syntax, axioms and theorems, within the overarching network of inheritance relationships. You can even work with these predicates directly, if you really want to. Locales are not an extension of higher-order logic; rather they are part of the Isar language.
One of the early motivations of locales was to assist in the structuring of large proofs. Typically the context is extended with various abstract objects about which assumptions are made, and these contexts are then further extended. Before the era of structured proofs, each claim was established as a separate, top-level theorem and proved by a shortish string of apply commands. Context management was clearly helpful with that approach. However, the Isar structured proof language was a much better solution: a proof of any length could be involve as many nested contexts as you needed, arising naturally through block structure. And such proofs were infinitely more legible.
But locales had another motivation at the very beginning: to formalise abstract algebra, groups, rings, fields, etc.: more generally, mathematical structures. A structure is a tuple consisting of one or more carrier sets bundled with some operations satisfying various laws. This can straightforwardly be represented by a logical predicate. In many cases, the underlying type of the carrier sets will either be obvious or can be a parameter of the locale. Because mathematical structures are frequently piled one atop another, Isabelle supports locale hierarchies, including multiple inheritance. A locale can be seen as a portable context that can be re-entered when needed, bringing with it associated syntax and facts. If this sounds similar to type classes, it’s because type classes are actually implemented as a special case of locales.
An example: abstract algebra
Let’s look at a new formalisation of abstract algebra, following a classic text and due to Clemens Ballarin. His paper walks through the example in full and begins with a brief but precise introduction to locale declarations (one far more authoritative than mine, by the way).
Declaring a locale of monoids
A monoid has a carrier set $M$, a composition (or product) operator and a unit. Concrete syntax is attached to the latter two elements. (Note that the 1 is a boldface symbol distinct from the integer 1.)
The declaration specifies the monoid axioms: the unit belongs to M and that set is closed under composition, etc.
Within the context of this locale, its components, concrete syntax and assumptions are visible.
Theorems proved within the locale become part of it and will be visible when monoid is next opened.
locale monoid = fixes M and composition (infixl "⋅" 70) and unit ("𝟭") assumes composition_closed [intro, simp]: "⟦ a ∈ M; b ∈ M ⟧ ⟹ a ⋅ b ∈ M" and unit_closed [intro, simp]: "𝟭 ∈ M" and associative [intro]: "⟦ a ∈ M; b ∈ M; c ∈ M ⟧ ⟹ (a ⋅ b) ⋅ c = a ⋅ (b ⋅ c)" and left_unit [intro, simp]: "a ∈ M ⟹ 𝟭 ⋅ a = a" and right_unit [intro, simp]: "a ∈ M ⟹ a ⋅ 𝟭 = a"
Given a particular monoid $M$, a submonoid is given by some $N\subseteq M$ satisfying the obvious closure properties.
locale submonoid = monoid M "(⋅)" 𝟭 for N and M and composition (infixl "⋅" 70) and unit ("𝟭") + assumes subset: "N ⊆ M" and sub_composition_closed: "⟦ a ∈ N; b ∈ N ⟧ ⟹ a ⋅ b ∈ N" and sub_unit_closed: "𝟭 ∈ N"
A simple example of a monoid is a monoid of transformations. Its elements are automorphisms of some given set $S$ (i.e. functions $S\to S$) with function composition as product and the identity function as unit.
locale transformations = fixes S :: "'a set"
Note that this locale has nothing but the set $S$. That it actually specifies a monoid we prove using a sublocale declaration, specifying the required monoid components. We obtain the monoid of all transformations on $S$.
sublocale transformations ⊆ monoid "S →⇩E S" "compose S" "identity S" by unfold_locales (auto simp: PiE_def compose_eq compose_assoc Id_compose compose_Id)
The sublocale declaration establishes that transformations is a monoid with the function space over S as the carrier set, function composition as the product and the identity function as the unit. (The second line is the proof of the necessary axioms.)
The declaration informs Isabelle that every instance of transformations is an instance of monoid.
It modifies the internal graph of locales as if the declaration has imported monoid explicitly. For another example, the declaration below
asserts that every submonoid is indeed a monoid, with carrier set N and the same monoid operations.
sublocale submonoid ⊆ sub: monoid N "(⋅)" 𝟭 by unfold_locales (auto simp: sub_composition_closed sub_unit_closed)
Again, the monoid axioms must be proved. I won’t discuss the (trivial) proof here other than to point out the proof method unfold_locales. It is the natural start of a locale instantiation proof, making explicit the properties that must be proved. There’s also intro_locales, which is similar but less explosive, unfolding only one level at a time.
Now we can declare a locale for a transformation monoid $M$ of $S$, where $M\subseteq S\to S$ is a subset of the automorphisms on $S$ containing the identity map and closed under composition.
The begin and end bracket some developments within the locale, here a trivial closure theorem with attached attributes (intro and simp) that will be operative in the locale.
locale transformation_monoid = transformations S + submonoid M "S →⇩E S" "compose S" "identity S" for M and S begin lemma transformation_closed [intro, simp]: "⟦ α ∈ M; x ∈ S ⟧ ⟹ α x ∈ S" by (metis PiE_iff sub) end
Groups and subgroups
A group is a monoid each of whose elements has an inverse. Within the context of the monoid locale—where the product and unit are available—we can define the property of being invertible and the inverse operator (the latter by a description) and prove theorems about them.
The set Units consists of all the invertible elements of M.
context monoid begin definition invertible where "u ∈ M ⟹ invertible u ⟷ (∃v ∈ M. u ⋅ v = 𝟭 ∧ v ⋅ u = 𝟭)" definition inverse where "inverse = (λu ∈ M. THE v. v ∈ M ∧ u ⋅ v = 𝟭 ∧ v ⋅ u = 𝟭)" definition "Units = {u ∈ M. invertible u}" end
Note: I reproduce Ballarin’s definition of invertible, which depends on the condition u ∈ M.
However, it’s not clear that making a definition conditional serves any real purpose.
If this particular condition is deleted, the development builds exactly as before.
A group $G$ is a monoid with a given product and unit (we specify the same syntax as before), satisfying an additional property: all elements of $G$ are invertible.
locale group = monoid G "(⋅)" 𝟭 for G and composition (infixl "⋅" 70) and unit ("𝟭") + assumes invertible [simp, intro]: "u ∈ G ⟹ invertible u"
Here we define the notion of a subgroup as a locale consisting of a group $G$ that is also a submonoid of some monoid $M$.
Within this locale, we prove two simple facts involving invertible and inverse.
locale subgroup = submonoid G M "(⋅)" 𝟭 + sub: group G "(⋅)" 𝟭 for G and M and composition (infixl "⋅" 70) and unit ("𝟭") begin lemma subgroup_inverse_equality [simp]: "u ∈ G ⟹ inverse u = sub.inverse u" by (simp add: inverse_equality) lemma subgroup_inverse_iff [simp]: "⟦ invertible x; x ∈ M ⟧ ⟹ inverse x ∈ G ⟷ x ∈ G" using invertible_inverse_inverse sub.invertible_inverse_closed by fastforce end
It’s fairly straightforward to prove that Units is a subgroup of M (within the monoid context).
We use an interpretation command, which is the basic mechanism for showing specific instances of locales. The proof—omitted, too much boilerplate—involves showing the underlying properties of the subgroup locale, e.g. that Units is closed under products.
interpretation units: subgroup Units M proof ... ... ... qed (auto simp: Units_def)
An interpretation can have a name, here units, to refer to the corresponding instances of the locale’s theorems.
Homomorphisms
An issue that arises in textbooks is how to disambiguate references to the product and unit when there are multiple groups. The following definition of a monoid homomorphism shows a simple solution: the two instances of the monoid locale are labelled source and target, and the names of the symbols for the target are decorated. The prime character (single quote) is written twice in the declaration because it is also used to escape special characters, in this case itself.
A homomorphism is a map $\eta$ that preserves the composition and unit operators.
locale monoid_homomorphism = map η M M'+ source: monoid M "(⋅)" 𝟭 + target: monoid M' "(⋅')" "𝟭'" for η and M and composition (infixl "⋅" 70) and unit ("𝟭") and M' and composition' (infixl "⋅''" 70) and unit' ("𝟭''") + assumes commutes_with_composition: "⟦ x ∈ M; y ∈ M ⟧ ⟹ η (x ⋅ y) = η x ⋅' η y" and commutes_with_unit: "η 𝟭 = 𝟭'"
And a tiny proof: every monoid homomorphism $\eta$ from $M$ to $M’$ determines a submonoid of $M’$, namely the image $\eta(M)$.
sublocale monoid_homomorphism ⊆ image: submonoid "η ` M" M' "(⋅')" "𝟭'" by unfold_locales (auto simp flip: commutes_with_composition commutes_with_unit)
There is much, much more in the full group theory development.
Records vs separate components
Isabelle/HOL has a substantial Algebra library, formalised long ago using locales but in an absolutely different style: representing structures by records. The intent was to avoid the repetition of argument lists, which we do see here, and which can get worse as definitions are stacked in higher and higher towers of Babel. Isabelle/HOL records are extensible, but they aren’t really flexible enough and by the time we get to rings—baby steps still—things already get ugly.
And here are rings under Ballarin’s approach:
locale ring = additive: abelian_group R "(+)" 𝟬 + multiplicative: monoid R "(⋅)" 𝟭 for R and addition (infixl "+" 65) and multiplication (infixl "⋅" 70) and zero ("𝟬") and unit ("𝟭") + assumes distributive: "⟦ a ∈ R; b ∈ R; c ∈ R ⟧ ⟹ a ⋅ (b + c) = a ⋅ b + a ⋅ c" "⟦ a ∈ R; b ∈ R; c ∈ R ⟧ ⟹ (b + c) ⋅ a = b ⋅ a + c ⋅ a"
In a landmark project led by Anthony Bordg, our team was able to formalise Grothendieck schemes, a feat many had thought to be impossible. We followed Ballarin’s approach consistently. To be honest, we did suffer a proliferation of ever longer argument lists in locales. But it does not seem beyond the wit of man to find some simple way to bundle them up. One can also argue whether turning everything into a locale is a good idea.
We’ve had these tools for nearly 20 years and are only now starting to explore their limits.
Postscript
Despite the limitations of type classes, it’s worth noting that the Isabelle distribution and its Archive of Formal Proofs contain more than 4000 type class instance declarations.
For a thorough introduction to locales, see Ballarin’s “Tutorial to Locales and Locale Interpretation”. It’s directly available from the documentation panel of your jEdit session. He also wrote a comprehensive, definitive journal article. My thanks to him for checking over this post.