types - 如何理解 agda 中的数据与记录功能？

Question

为什么自定义单位类型不允许我们证明这个基本的左单位定律？我看到我的实现与标准库的实现之间的唯一区别是使用了RecordvsData归纳归纳类型模型。我不明白为什么Data不允许我证明这个基本的左身份引理，这在定义上应该是正确的。它与Record的自动 eta 继承有关吗？如果是这样，为什么会这样？Record如果没有内置（例如）单元类型，是否可以证明这一点？一般来说，这是 的限制Data，还是可以在 agda 模记录中做所有事情？

data _≡_ {A : Set} : A → A → Set where
  refl : (a : A) → a ≡ a

--from builtin
lunitm : (f : ⊤ → ⊤) → (λ x → f tt) ≡ f
lunitm f = refl (λ x → tt)

data ⊤2 : Set where
  tt2 : ⊤2

lunitm2 : (f : ⊤2 → ⊤2) → (λ x → f tt2) ≡ f
lunitm2 f = ? --refl ? --can't instantiate

标签： typesrecordagdatype-theory

Answer 1

这确实是由于⊤2是 adata而不是record。

Agda 为否定类型实现了 eta 规则。

记录是负面的，因此有与之相关的 eta 规则。的 eta 规则

record Unit : Set where
  constructor unit

是

_ : (u : Unit) -> u ≡ unit
_ = λ u -> refl

理论上支持正类型的 eta-equality 是可能的，但 Agda 没有实现这一点。