haskell - 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

谢谢你给我的礼物!

最佳答案

A Cosmology of Datatypes的“7.3.2。导出数据类型的操作”一章显示了如何使用描述来导出操作。但是，派生的Eq在那儿比较弱。

基本思想是使用某种一阶编码(即根据某种通用数据类型)表示数据类型，并定义对此数据类型的操作，因此，根据该通用数据类型进行编码的所有内容都可以由这些通用操作处理。我详细介绍了该机制here的简单版本。

如果您有封闭的Universe，则可以派生更强的Eq。使用类似于描述的方法(应该具有同等的表达力，但我没有检查)并在一个封闭的Universe中定义了通用的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)“刷新”了ℓ。

更新:show链接现在已断开(我应该使用永久链接)。但是，现在有一个更好的示例:an entire library，它为常规Agda数据类型派生Eq。

关于haskell - Agda的Haskell派生机制，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/36209339/