Agda records: псевдоним поля - PullRequest
Новая
       7

Agda records: псевдоним поля

0 голосов
/ 10 июня 2018

Я пишу свою собственную формализацию базовой алгебры в Агде.Я определил следующее: 

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

Теперь я хочу определить кольца, наследуемые от этого: 

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>

Конечно, проблемная строка - это то, где я присваиваю _+_ вобъявление записи звонка, потому что я не могу присвоить значения в простом определении типа, как это.

Что я хочу сделать, это не дать конструктор для _+_, а вместо этого сделать его автоматически доступным какполе (и его значение равно полю _._ в additiveGroup) всякий раз, когда строится ring.В объектно-ориентированном мире это, вероятно, просто метод для класса.

Учебное пособие Чалмерса по записям , похоже, не дает ответа; стандартная библиотека , кажется, делает это вместо этого, определяя кольцо как запись со всей структурой группы на верхнем уровне вместе с доказательством того, что компоненты структуры группы действительно формируют группу.Я думаю, что это немного грязно, так как у нас уже есть тип, который представляет группы;это может быть чище, если запись звонка может попасть в группу, которую она содержит.Это возможно?

1 Ответ

0 голосов
/ 10 июня 2018

Вы можете дать любые определения внутри объявления записи, а не только поля.Просто убедитесь, что они не попадают под блок field: 

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

Это очень похоже на метод класса в языке OO.Вы можете даже дать больше полей после определений, начав новый блок field.

...