AGDA：如何告诉类型系统两种类型相等？

发布于 2025-02-02 23:09:30 字数 599 浏览 1 评论 0原文

说我的类型依赖于NAT

data MyType : (i : ℕ) → Set where
  cons : (i : ℕ) → MyType i

和一个功能：

combine : {i₁ i₂ : ℕ} → MyType i₁ → MyType i₂ → MyType (i₁ ⊔ i₂)

现在我正在尝试编写一个功能：

create-combined : (i : ℕ) → MyType i
create-combined i = combine {i} {i} (cons i) (cons i)

不幸的是，我收到错误消息：

i ⊔ i != i of type ℕ
when checking that the inferred type of an application
  MyType (i ⊔ i)
matches the expected type
  MyType i

我知道我可以证明i⊔i≡i。 ''知道如何将该证明提供给类型系统以解决此问题。

我该如何汇编？

原文

Say I have type dependent on Nat

data MyType : (i : ℕ) → Set where
  cons : (i : ℕ) → MyType i

and a function:

combine : {i₁ i₂ : ℕ} → MyType i₁ → MyType i₂ → MyType (i₁ ⊔ i₂)

Now I'm trying to write a function:

create-combined : (i : ℕ) → MyType i
create-combined i = combine {i} {i} (cons i) (cons i)

Unfortunately, I get the error message:

i ⊔ i != i of type ℕ
when checking that the inferred type of an application
  MyType (i ⊔ i)
matches the expected type
  MyType i

I know I can prove i ⊔ i ≡ i, but I don't know how to give that proof to the type system in order to get this to resolve.

How do I get this to compile?

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

近箐 2025-02-09 23:09:30

您可以从relation.binary.binary.propositionalequality中使用替代。

给它：

证明i⊔i
。
您 组合{i} {i}（cons i）（cons i）

，或者您可以在证明上也可以使用重写关键字，通常是优选的。

这是对向量串联应用的两种可能性的（人为）示例：

module ConsVec where

open import Data.Vec
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality

_++₁_ : ∀ {a} {A : Set a} {m n} → Vec A m → Vec A n → Vec A (n + m)
_++₁_ {m = m} {n} v₁ v₂ = subst (Vec _) (+-comm m n) (v₁ ++ v₂)

_++₂_ : ∀ {a} {A : Set a} {m n} → Vec A m → Vec A n → Vec A (n + m)
_++₂_ {m = m} {n} v₁ v₂ rewrite sym (+-comm m n) = v₁ ++ v₂

You can use subst from Relation.Binary.PropositionalEquality.

You give it:

the proof that i ⊔ i ≡ i
the dependent type that should be transformed with the proof, in your case MyType
the term to be transformed, in your case combine {i} {i} (cons i) (cons i)

Or you can use the rewrite keyword as well on your proof, which is usually to be preferred.

Here is an (artificial) example of both possibilities applied on vector concatenation:

module ConsVec where

open import Data.Vec
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality

_++₁_ : ∀ {a} {A : Set a} {m n} → Vec A m → Vec A n → Vec A (n + m)
_++₁_ {m = m} {n} v₁ v₂ = subst (Vec _) (+-comm m n) (v₁ ++ v₂)

_++₂_ : ∀ {a} {A : Set a} {m n} → Vec A m → Vec A n → Vec A (n + m)
_++₂_ {m = m} {n} v₁ v₂ rewrite sym (+-comm m n) = v₁ ++ v₂

回复收藏 0 原文

~没有更多了~