Stream: Beginner Questions

Topic: Should I always bundle the data in a locale into a record?

James Hanson (Mar 01 2024 at 01:24):

In HOL-Algebra, algebraic objects are typically implemented as a record and then a locale. For example, monoids are defined like this:

record 'a monoid =  "'a partial_object" +
  mult    :: "['a, 'a] ⇒ 'a" (infixl "⊗ı" 70)
  one     :: 'a ("𝟭ı")

With the corresponding locale a little bit later:

locale monoid =
  fixes G (structure)
  assumes m_closed [intro, simp]:
         "⟦x ∈ carrier G; y ∈ carrier G⟧ ⟹ x ⊗ y ∈ carrier G"
      and m_assoc:
         "⟦x ∈ carrier G; y ∈ carrier G; z ∈ carrier G⟧
          ⟹ (x ⊗ y) ⊗ z = x ⊗ (y ⊗ z)"
      and one_closed [intro, simp]: "𝟭 ∈ carrier G"
      and l_one [simp]: "x ∈ carrier G ⟹ 𝟭 ⊗ x = x"
      and r_one [simp]: "x ∈ carrier G ⟹ x ⊗ 𝟭 = x"

If I were defining monoids myself, my naive instinct might be to just define the locale monoid as a locale fixing the relevant data directly:

locale monoid =
  fixes
    carrier :: "'a set"
    mult :: "['a, 'a] ⇒ 'a"
    one :: 'a
  assumes
    ...

One minor advantage of this would be the ability to write carrier instead of carrier G all of the time.

I know there must be a good reason why HOL-Algebra is set up the way that it is, but I don't have a good enough grasp of structuring larger projects to see it. Why is this done this way, and would there ever be a situation in which I would want to just fix the data in the locale directly?

Manuel Eberl (Mar 01 2024 at 14:37):

This is exactly what Clemens Ballarin's new algebra approach does: https://www.isa-afp.org/entries/Jacobson_Basic_Algebra.html There is also an accompanying paper. You might also find some interesting discussion on that approach in the paper by @Anthony Bordg et al. about schemes.

One advantage of the record-style approach of HOL-Algebra is that it is easier to make a function that returns e.g. a group. Another might be that syntax is more uniform, although it has to be said that the syntax can become quite cumbersome quite quickly with HOL-Algebra as well…

Manuel Eberl (Mar 01 2024 at 14:38):

At the end of the day I would say that both approaches are valid and have their pros and cons. I personally am a bit more in favour of the old HOL-Algebra style with records, but I'm not super happy with either approach.

Wenda Li (Mar 01 2024 at 21:10):

Using a record is fine as long as you don't abuse the inheritance feature of it as discussed in Ballarin's paper.

Last updated: Apr 28 2024 at 04:17 UTC