Ищите объяснение неявного типа функции против явного типа функции - PullRequest
Новая
       61

Ищите объяснение неявного типа функции против явного типа функции

1 голос
/ 07 ноября 2019

Учитывая следующую подпись модуля 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 }

Доказательство транзитивности - это то, что вызывает у меня вопрос. Предыдущее определение принято Агдой, а отклонено следующее: 

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

В качестве примечания второй стороны, яЯ знаю, что на подобный вопрос уже был дан ответ:

Как обойти неявную или явную ошибку типа функции?

Но указанный ответ не содержит какого-либо глубокого объясненияоб этом удивительном поведении.

...