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？而且是有什么样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 coerce通过这样的方式来处理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工作原理; 这很有启发性.