agda：如何告诉类型系统两种类型是相等的？

Question

假设我的类型依赖于 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，但我不知道如何将证明提供给类型系统以解决此问题。

如何编译它？

Answer 1

您可以使用 Relation.Binary.PropositionalEquality 中的 subst。

你给它：

证明 i ⊔ i ≡ i
应该用证明转换的依赖类型，在你的例子中MyType
要转换的术语，在您的情况下combine {i} {i} (cons i) (cons i)

或者您也可以在证明中使用 rewrite 关键字，这通常是首选。

这是一个（人工）示例，说明了两种可能性都适用于向量串联：

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₂

agda：如何告诉类型系统两种类型是相等的？

agda: How do I tell the type system that two types are equal?

agda