gpt4 book ai didi

Agda 的 Haskell 推导机制

转载 作者:行者123 更新时间:2023-12-02 02:22:45 27 4
gpt4 key购买 nike

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

可以推导出更强的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 (α ⊔ ℓ)对于任何 .所以当你有 ℕ : SetSet : Set₁ , 你想解除 来自 SetSet₁ , 这只是 Lift ℕ — 在简单的情况下,您不需要提供 明确地。

构造包装在 Lift 中的数据类型的元素您使用 lift (如 lift 0 中)。要获取此元素,请使用 lower , 所以 liftlower互为倒数。请注意 lift (lower x)不一定与 x 位于同一个宇宙中, 因为 lift (lower x) “刷新” .

更新 : show链接现在已损坏(我应该使用永久链接)。但现在有一个更好的例子: an entire library派生出 Eq用于常规 Agda 数据类型。

关于Agda 的 Haskell 推导机制,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/36209339/

27 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com