Механизм получения Haskell для Agda

Question

Мне интересно, есть ли в Агде что-нибудь похожее на Хаскелла? deriving Eq пункт --- тогда у меня есть связанный вопрос также.

Например, предположим, у меня есть типы для игрушечного языка,

data Type : Set where
  Nat  : Type
  Prp : Type

Тогда я могу реализовать разрешимое равенство путем сопоставления с образцом и C-c C-a,

_≟ₜ_ : Decidable {A = Type} _≡_
Nat ≟ₜ Nat = yes refl
Nat ≟ₜ Prp = no (λ ())
Prp ≟ₜ Nat = no (λ ())
Prp ≟ₜ Prp = yes refl

Мне любопытно, может ли это быть механизировано или автоматизировано так же, как это делается в Haskell:

data Type = Nat | Prp deriving Eq

Спасибо!

Пока мы говорим о типах, я хотел бы реализовать свои формальные типы как типы Agda: Nat - это просто натуральные числа, а Prp - небольшие предложения.

⟦_⟧Type : Type → Set ?
⟦ Nat ⟧Type = ℕ
⟦ Prp ⟧Type = Set

К сожалению, это не работает. Я пытался исправить это с помощью подъема, но потерпел неудачу, так как понятия не имею, как использовать подъем уровня. Любая помощь приветствуется!

Пример использования вышеуказанной функции:

record InterpretedFunctionSymbol : Set where
  field
   arity   : ℕ
   src tgt : Type
   reify   : Vec ⟦ src ⟧Type arity → ⟦ tgt ⟧Type

Спасибо тебе за то, что ублажаешь меня!

Answer 1

Глава "7.3.2. Деривация операций над типами данных" в главе " Космология типов данных" показывает, как вывести операции с использованием описаний. Хотя, производный Eq там довольно слабый

Основная идея состоит в том, чтобы представлять типы данных с использованием некоторого кодирования первого порядка, то есть в терминах некоторого универсального типа данных, и определять операции с этим типом данных, чтобы все кодированные в терминах этого типа могли обрабатываться этими универсальными операциями. Я разработал простую версию этого механизма здесь.

Вы можете получить более сильный Eq, если у вас есть закрытая вселенная. Используя подход, аналогичный описанию (должен быть одинаково выразительным, но я не проверял) и закрытую вселенную, которую я определил как универсальную show здесь, что позволяет, например, напечатать вектор кортежей после того, как вы назовете конструкторы:

instance
  named-vec : {A : Type} -> Named (vec-cs A)
  named-vec = record { names = "nil" ∷ "cons" ∷ [] }

test₂ : show (Vec (nat & nat) 3 ∋ (7 , 8) ∷ᵥ (9 , 10) ∷ᵥ (11 , 12) ∷ᵥ []ᵥ)
      ≡ "(cons 2 (7 , 8) (cons 1 (9 , 10) (cons 0 (11 , 12) nil)))"
test₂ = prefl

где Vec определяется с точки зрения аналога Desc тип данных. Eq Дело должно быть похожим, но более сложным.

Вот как Lift может быть использован:

⟦_⟧Type : Type → Set₁
⟦ Nat ⟧Type = Lift ℕ
⟦ Prp ⟧Type = Set

ex₁ : ∀ A -> ⟦ A ⟧Type
ex₁ Nat = lift 0
ex₁ Prp = ℕ

ex₂ : ∀ A -> ⟦ A ⟧Type -> Maybe ℕ
ex₂ Nat n = just (lower n) -- or (ex₂ Nat (lift n) = just n)
ex₂ Prp t = nothing

Если A : Set α затем Lift A : Set (α ⊔ ℓ) для любого ℓ, Итак, когда у вас есть ℕ : Set а также Set : Set₁хочешь поднять ℕ от Set в Set₁что просто Lift ℕ - в простых случаях вам не нужно предоставлять ℓ в явном виде.

Чтобы создать элемент типа данных, завернутый в Lift ты используешь lift (как в lift 0). И чтобы вернуть этот элемент вы используете lower, так lift а также lower являются противоположностями друг друга. Обратите внимание, что lift (lower x) не обязательно лежат в той же вселенной, что и x, так как lift (lower x) "освежают" ℓ,

Answer 2

Для практической реализации "получения Eq" в Agda вы можете взглянуть на agda-prelude Ульфа по адресу https://github.com/UlfNorell/agda-prelude. В частности, модуль Tactic.Deriving.Eq содержит код для автоматической генерации разрешимого равенства для довольно общего класса (простых и индексированных) типов данных.