Agda records: field alias

Question

I am writing my own formalisation of basic algebra in Agda. I've defined the following:

record group {a} {A : Set a} : Set a where
  infixl 7 _·_
  field
      _·_ : A → A → A
      <many other laws>

Now I want to define rings inheriting from this:

record ring {a} {A : Set a} : Set a where
  infixl 6 _+_
  infixl 8 _*_
  field
    additiveGroup : group A
    _*_ : A → A
    _+_ = additiveGroup._._
    <the other ring-specific laws, not the group laws>

Of course, the problematic line is where I assign to _+_ in the ring record declaration, because I can't assign values in a mere type definition like this.

What I want to do is to not give a constructor for _+_, but instead have it automatically available as a field (and have its value equal to the _._ field on additiveGroup) whenever a ring is constructed. In the object-oriented world, this would probably just be a method on the class.

The Chalmers tutorial on records doesn't seem to give an answer; the standard library appears to do this instead by defining a ring to be a record with all the group structure at the top level, along with a proof that the group structure components do form a group. I think this feels a bit messy since we already have a type which represents groups; it might be cleaner if the ring record could reach down into a group it contains. Is this possible?

Jesper Jesper · Accepted Answer · 2018-06-10T11:38:24

You can give any definitions inside a record declaration, not just fields. Just make sure they don't fall under the field block:

record ring {a} {A : Set a} : Set a where
  infixl 6 _+_
  infixl 8 _*_
  field
    additiveGroup : group A
    _*_ : A → A
  _+_ = group._._ additiveGroup

This works very much like a class method in an OO language. You can even give more fields after the definitions by starting a new field block.

Agda records: field alias

1 Answers