Haskell Agda 的派生机制

Question

我想知道 Agda 中是否有任何类似于 Haskell 的 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

A Cosmology of Datatypes 的“7.3.2. 推导数据类型的操作”一章展示了如何使用描述推导操作。虽然，派生的Eq在那里相当弱。

基本思想是使用一些一阶编码来表示数据类型，即根据一些通用数据类型，并定义对该数据类型的操作，因此根据它编码的所有内容都可以由这些通用数据类型处理操作。我详细阐述了这个机器的一个简单版本 here.

如果你有一个封闭的宇宙，你可以获得更强的Eq。使用类似于描述的方法（应该同样具有表现力，但我没有检查）和一个封闭的宇宙我定义了通用 show here，它允许例如在命名构造函数后打印元组向量：

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) "refreshes" ℓ.

更新：show link 现在坏了（我应该用 permalink）。但是现在有一个更好的例子：an entire library 为常规 Agda 数据类型导出 Eq。

Answer 2

要在 Agda 中实际实现 "deriving Eq"，您可以在 https://github.com/UlfNorell/agda-prelude 查看 Ulf 的 agda-prelude。特别是，模块 Tactic.Deriving.Eq 包含为相当普遍的 class 数据类型（简单和索引）自动生成可判定相等性的代码。

Haskell Agda 的派生机制

Haskell Deriving Mechanism for Agda

haskell

signature

agda