问题描述
我想知道Agda中是否有类似于Haskell的派生Eq 子句的东西---那么我也有下面的相关问题。
b$ b
例如，假设我有一个玩具语言的类型，
数据类型：设置其中
Nat：Type
Prp：Type
然后我可以实现可确定通过模式匹配和 Cc Ca ，
___：Decicable {A = Type}_≡_
Nat≟ₜNat = yes refl
Nat≟ₜPrp = no（λ（））
Prp≟ₜNat = no（λ（））
Prp≟ₜPrp =是refl
我很好奇这是否可以机械化或自动化与Haskell的方式类似：
data Type = Nat | Prp派生出Eq
谢谢！
虽然我们谈到类型的话题，但我想要将我的正式类型看作Agda类型：Nat只是自然数，而Prp是小命题。
⟦_⟧Type：Type→Set？
⟦Nat⟧Type=ℕ
⟦Prp⟧Type= Set
悲哀地这不起作用。我试图用提升来解决这个问题，但是因为我对如何使用水平提升毫无头绪。任何帮助表示赞赏！
以上函数的一个示例用法是，
record InterpretedFunctionSymbol：设置其中
字段
arity：ℕ
src tgt：输入
reify：Vec⟦src⟧类型arity→⟦tgt⟧Type
感谢您对我的侮辱！
$ b
基本思想是使用一些first-顺序编码（即根据某种通用数据类型），并定义对该数据类型的操作，因此所有以此为依据的编码都可以由这些通用操作来处理。我在这里阐述了这个机制的简单版本。
如果您有一个封闭的Universe，则可以派生更强的 Eq 。使用类似描述的方法（应该具有同样的表现力，但我没有检查）和封闭的宇宙，我定义了通用的 show ，它允许例如在命名构造函数后打印一个元组向量：
instance
named-vec：{A：Type} - >名称（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）无）））
test2 = prefl
其中 Vec 的定义类似于 Desc 数据类型。 Eq 情况应该是相似的，但更复杂一些。
以下是 Lift 可以使用：
⟦_⟧Type：Type→Set 1
⟦Nat⟧Type = Liftℕ
⟦Prp⟧Type= Set
ex 1：∀A - > ⟦A⟧Type
ex 1 Nat =电梯0
ex 1 Prp =ℕ
ex₂：∀A - > ⟦A⟧Type - >也许ℕ
ex ex n n =正好（低n） - 或（ex n Nat（抬n）=正n）
ex 2 Prp t =没有
如果 A：设置α，则 Lift A：Set（α⊔ℓ ）适用于任何ℓ。所以当你有ℕ：Set 和 Set：Set 1 时，你想提升ℕ从设置到 Set 1 ，这只是提升ℕ code> - 在简单情况下，您不需要明确提供ℓ。
包含在 Lift中的数据类型元素您可以使用 lift （如 lift 0 ）。并且为了得到这个元素，可以使用 lower ，所以 lift 和 lower 是彼此相反的。但请注意， lift（lower x）不一定与 x 位于同一个Universe中，因为 lift（lower x）刷新ℓ。
I am wondering if there is anything in Agda that resembles Haskell's deriving Eq clause ---then I have an associated question below, as well.
For example, suppose I have types for a toy-language,
data Type : Set where Nat : Type Prp : Type
Then I can implement decidable equality by pattern matching and C-c C-a,
_≟ₜ_ : Decidable {A = Type} _≡_
Nat ≟ₜ Nat = yes refl
Nat ≟ₜ Prp = no (λ ())
Prp ≟ₜ Nat = no (λ ())
Prp ≟ₜ Prp = yes refl
I'm curious if this can be mechanised or automated somehow similar to the manner it is done in Haskell:
data Type = Nat | Prp deriving Eq
Thank-you!
While we're on the topic of types, I'd like to realise my formal types as Agda types: Nat is just natural numbers while Prp is small propositions.
⟦_⟧Type : Type → Set ? ⟦ Nat ⟧Type = ℕ ⟦ Prp ⟧Type = Set
Sadly this does not work. I tried to fix this with lifting but failed since I haven't a clue on how to use level lifting. Any help is appreciated!
An example usage of the above function would be,
record InterpretedFunctionSymbol : Set where field arity : ℕ src tgt : Type reify : Vec ⟦ src ⟧Type arity → ⟦ tgt ⟧Type
Thank-you for humouring me!
The "7.3.2. Deriving operations on datatypes" chapter of A Cosmology of Datatypes shows how to derive operations using descriptions. Though, the derived Eq is rather weak there.
The basic idea is to represent data types using some first-order encoding, i.e. in terms of some generic data type, and define operations on this data type, so everything encoded in terms of it can be handled by these generic operations. I elaborated a simple version of this machinery here.
You can derive a stronger Eq, if you have a closed universe. Using a similar to descriptions approach (should be equally expressive, but I didn't check) and a closed universe I defined generic show here, which allows e.g. to print a vector of tuples after you name the constructors:
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 is defined in terms of a similar to Desc data type. The Eq case should be similar, but more sophisticated.
Here is how Lift can be used:
⟦_⟧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 (α ⊔ ℓ) for any ℓ. So when you have ℕ : Set and Set : Set₁, you want to lift ℕ from Set to Set₁, which is just Lift ℕ — in simple cases you don't need to provide ℓ explicitly.
To construct an element of a data type wrapped in Lift you use lift (like in lift 0). And to get this element back you use lower, so lift and lower are inverses of each other. Note though that lift (lower x) doesn't necessarily lie in the same universe as x, because lift (lower x) "refreshes" ℓ.
这篇关于Agda的Haskell派生机制的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！