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

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

0 голосов
/ 29 мая 2019

Это из последней главы книги PLFA. 

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open import Data.Product using (_×_; ∃; ∃-syntax; Σ; Σ-syntax) renaming (_,_ to ⟨_,_⟩)

infix 0 _≃_
record _≃_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_

data List (A : Set) : Set where
  []  : List A
  _∷_ : A → List A → List A

infixr 5 _∷_

data All {A : Set} (P : A → Set) : List A → Set where
  []  : All P []
  _∷_ : ∀ {x : A} {xs : List A} → P x → All P xs → All P (x ∷ xs)

data Any {A : Set} (P : A → Set) : List A → Set where
  here  : ∀ {x : A} {xs : List A} → P x → Any P (x ∷ xs)
  there : ∀ {x : A} {xs : List A} → Any P xs → Any P (x ∷ xs)

infix 4 _∈_

_∈_ : ∀ {A : Set} (x : A) (xs : List A) → Set
x ∈ xs = Any (x ≡_) xs

All-∀ : ∀ {A : Set} {P : A → Set} {xs} → All P xs ≃ (∀ {x} → x ∈ xs → P x)
All-∀ {A} {P} =
  record { to = to'
         ; from = from'
         ; from∘to = from∘to'
         ; to∘from = to∘from'
         }
  where
    to' : ∀ {xs} → All P xs → (∀ {x} → x ∈ xs → P x)
    from' : ∀ {xs} → (∀ {x} → x ∈ xs → P x) → All P xs

    from∘to' : ∀ {xs : List A} → (x : All P xs) → from' (to' x) ≡ x
    to∘from' : ∀ {xs : List A} → (x∈xs→Px : ∀ {x} → x ∈ xs → P x) → to' (from' x∈xs→Px) ≡ x∈xs→Px

Когда я заполняю отверстие с помощью to (from x∈xs→Px) ≡ x∈xs→Px, я получаю следующую ошибку. 

_x_1668 (x∈xs→Px = x∈xs→Px) ∈ xs → P (_x_1668 (x∈xs→Px = x∈xs→Px))
!= {x : A} → x ∈ xs → P x because one is an implicit function type
and the other is an explicit function type
when checking that the expression to∘from has type
(y : {x : A} → x ∈ xs → P x) → to (from y) ≡ y

Я не уверен, что это значит, но Агда может быть сомнительной, когда вовлекаются неявные аргументы.Единственное, что я не пробовал, это заменить {x} на (x) в ∀ {x} → x ∈ xs → P x, потому что это является частью определения проблемы.

Какой здесь должна быть сигнатура типа?Также существует ли более простой способ сделать это, чем where блок для каждой функции в изоморфизме?Мне не нравится интенсивное копирование сигнатур типа.

1 Ответ

0 голосов
/ 03 июня 2019

Даже с учетом того, что @gallais сказал на странице Agda, мне понадобилось почти 3 часа, чтобы понять, как это сделать.Вот что я бы порекомендовал подписи типа.Я столкнулся с большими проблемами с функциональностью расширения.Фактическая проблема была тривиальной в сравнении.

Я думаю, что способ работы логического вывода для неявных аргументов может определенно использовать некоторое обслуживание. 

postulate
  extensionality : ∀ {A : Set} {B : A → Set} {f g : (x : A) → B x}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

postulate
  extensionality_impl : ∀ {X : Set}{Y : X → Set}
                  → {f g : {x : X} → Y x}
                  → ((x : X) → f {x} ≡ g {x})
                  → (λ {x} → f {x}) ≡ g

All-∀ : ∀ {A : Set} {P : A → Set} {xs} → All P xs ≃ (∀ {x} → x ∈ xs → P x)
All-∀ {A} {P} =
  record { to = to
         ; from = from
         ; from∘to = from∘to
         ; to∘from = λ x'∈xs→Px → extensionality_impl λ x → extensionality λ x∈xs → to∘from x'∈xs→Px x∈xs
         }
  where
    to : ∀ {xs} → All P xs → (∀ {x} → x ∈ xs → P x)
    from : ∀ {xs} → (∀ {x} → x ∈ xs → P x) → All P xs
    from∘to : ∀ {xs : List A} → (x : All P xs) → from (to x) ≡ x
    to∘from : ∀ {xs : List A} (x∈xs→Px : ∀ {x} → x ∈ xs → P x) {x} (x∈xs : x ∈ xs) → to (from x∈xs→Px) x∈xs ≡ x∈xs→Px x∈xs
...