Agda型安全铸造/强制

Question

我找到了一个有用的功能：

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

使用索引类型定义函数时。在索引不明确等于i，e的情况下，必须使用引理来显示类型匹配。

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函数。然而，这是一个更一般的函数的特例-- subst ( Relation.Binary.PropositionalEquality的等式的代换性质)

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处理这样的rewrite。

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是如何工作的；这很有启发性。