Agda 的 Haskell 推导机制

我想知道 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

谢谢你逗我开心！

的“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

where 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

If A : Set α then Lift A : Set (α ⊔ ℓ)对于任何ℓ。所以当你有ℕ : Set and Set : Set₁，你想举起ℕ from Set to Set₁，这只是Lift ℕ— 在简单的情况下你不需要提供ℓ明确地。

构造包装在其中的数据类型的元素Lift你用lift（像lift 0）。要取回这个元素，您可以使用lower, so lift and lower是互为倒数的。但请注意lift (lower x)不一定位于同一个宇宙x， 因为lift (lower x)“刷新”ℓ.

UPDATE: the show链接现在已损坏（我应该使用永久链接）。但现在有一个更好的例子：整个图书馆从而得出Eq对于常规 Agda 数据类型。