Учитывая следующую сигнатуру модуля agda:
module EqList {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} (eq≈ : IsEquivalence _≈_) where
Мы можем определить членство в списке, включение в список и эквивалентность списка:
_∈_ : REL A (List A) _
_∈_ x = Any (x ≈_)
_⊑_ : Rel (List A) _
_⊑_ = _⊆_ on flip _∈_
_≋_ : Rel (List A) _
_≋_ = _⊑_ -[ _×_ ]- flip _⊑_
Затем мы можем перейти к доказательству того, что это последнее отношение действительно является отношением эквивалентности:
isEq≋ : IsEquivalence _≋_
isEq≋ = record {
refl = id , id ;
sym = swap ;
trans = zip (λ f g → g ∘ f) λ f g → f ∘ g }
У меня возникает вопрос о доказательстве транзитивности. Предыдущее определение принимается Agda, а следующее отклоняется:
trans = zip (flip _∘_) _∘_
Ошибка следующая:
({x : A} → Any (_≈_ x) i → Any (_≈_ x) j) !=
((x : A) → Any (_≈_ x) j) because one is an implicit function type
and the other is an explicit function type
when checking that the expression _∘_ has type
(x : j ⊑ k) (y : i ⊑ j) → i ⊑ k
Хотя эта ошибка кажется странной, потому что оба доказательства должны быть эквивалентными (замена выражения f выражением λ x → f x всегда должна давать один и тот же результат), я могу несколько понять, почему это ведет себя таким образом: есть внутренние проблемы с тем, как создать различные неявные аргументы _∘_. Но это объяснение интуитивно понятно и не очень убедительно, поэтому мой вопрос следующий:
Может ли кто-нибудь подробно объяснить, почему проверка типов преуспевает в первом случае, а не во втором?
В качестве примечания, вот заголовок модуля, чтобы этот пример был самодостаточным:
open import Relation.Binary.Core
open import Data.List hiding (zip)
open import Data.List.Any
open import Relation.Unary using (_⊆_)
open import Function
open import Data.Product
В качестве второго примечания, я знаю, что на аналогичный вопрос уже был дан ответ:
Как обойти неявный или явный тип функции ошибка?
Но указанный ответ не содержит каких-либо подробных объяснений этого удивительного поведения.
