Agda type-safe cast / coercion

Question

I found handy a function:

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

when defining functions with indexed types. In situations where indexes are not definitionally equal i,e, one have to use lemma, to show the types match.

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

Note, yet this example is easy to rewrite so one don't need to coerce:

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

Sometimes pattern matching doesn't help though.

The question: But I wonder, whether something like that functions is already in agda-stdlib? And is there something like hoogle for Agda, or something like SearchAbout?

Vitus Vitus · Accepted Answer · 2015-01-05T23:00:48

I don't think there is exactly your coerce function. However, it's a special case of a more general function - subst (the substitutive property of equality) from 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

If you choose P = id (from Data.Function, or just write λ x → x), you get:

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

By the way, the most likely reason you won't find this function predefined, is that Agda deals with coerces like that through 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

This is a syntactic sugar for the more complicated:

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

If you are familiar with how with works, try to figure out how rewrite works; it's quite enlightening.

Agda type-safe cast / coercion

1 Answers