阿格達類型安全的鑄造/脅迫

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？有沒有像ho阿格達，或類似SearchAbout？

Answer 1

我不認爲你的coerce功能完全相同。然而，這是一個更一般的功能的一種特殊情況 - 從Relation.Binary.PropositionalEqualitysubst（平等的替代屬性）：

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 

---

順便說，最可能的原因，你不會找到這個函數預定義的，是與coerce就像通過阿格達交易：

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工程;這很有啓發性。