Agda 类型安全的转换/强制转换

Question

我找到了一个方便的函数：

coerce : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
coerce refl x = x

定义带有索引类型的函数时。在索引定义不相等的情况下，即必须使用引理来显示类型匹配。

zipVec : ∀ {a b n m } {A : Set a} {B : Set b} → Vec A n → Vec B m → Vec (A × B) (n ⊓ m)
zipVec [] _ = []
zipVec {n = n} _ [] = coerce (cong (Vec _) (0≡n⊓0 n)) []
zipVec (x ∷ xs) (y ∷ ys) = (x , y) ∷ zipVec xs ys

注意，但是这个例子很容易重写，所以不需要强制：

zipVec : ∀ {a b n m } {A : Set a} {B : Set b} → Vec A n → Vec B m → Vec (A × B) (n ⊓ m)
zipVec [] _ = []
zipVec (_ ∷ _) [] = []
zipVec (x ∷ xs) (y ∷ ys) = (x , y) ∷ zipVec xs ys

有时模式匹配并没有帮助。

问题：但是我想知道，agda-stdlib中是否已经有类似的功能？ Agda 有没有类似 hoogle 的东西，或者像 SearchAbout?

这样的东西

Answer 1

我认为您的 coerce 功能不完全相同。但是，它是更一般函数的特例 - 来自 Relation.Binary.PropositionalEquality:

的 subst（等式的替代属性）

subst : ∀ {a p} {A : Set a} (P : A → Set p) {x y : A}
      → x ≡ y → P x → P y
subst P refl p = p

如果您选择 P = id（来自 Data.Function，或者只写 λ x → x），您将得到：

coerce : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
coerce = subst id

顺便说一下，你找不到这个预定义函数的最可能原因是 Agda 通过 rewrite:

来处理 coerces

postulate
  n⊓0≡0 : ∀ n → n ⊓ 0 ≡ 0

zipVec : ∀ {a b n m} {A : Set a} {B : Set b}
       → Vec A n → Vec B m → Vec (A × B) (n ⊓ m)
zipVec [] _ = []
zipVec {n = n} _ [] rewrite n⊓0≡0 n = []
zipVec (x ∷ xs) (y ∷ ys) = (x , y) ∷ zipVec xs ys

这是更复杂的语法糖：

zipVec {n = n} _ [] with n ⊓ 0 | n⊓0≡0 n
... | ._ | refl = []

如果您熟悉 with 的工作原理，请尝试弄清楚 rewrite 的工作原理；很有启发性。

Agda 类型安全的转换/强制转换

Agda type-safe cast / coercion

agda