Problemi con l'utilizzo di coppie dipendenti in Agda

Question

Sto imparando Agda by tutorial e ora sto leggendo sulle coppie dipendenti.

Quindi, questo è il frammento di codice:

data Σ (A : Set) (B : A → Set) : Set where 
    _,_ : (a : A) → (b : B a) → Σ A B 

infixr 4 _,_ 

Σprojₗ : {A : Set}{B : A → Set} → Σ A B → A 
Σprojₗ (a , b) = a 

data _∈_ {A : Set}(x : A) : List A → Set where 
    first : {xs : List A} → x ∈ x ∷ xs 
    later : {y : A}{xs : List A} → x ∈ xs → x ∈ y ∷ xs 

infix 4 _∈_ 

_!_ : ∀{A : Set} → List A → ℕ → Maybe A 
    [] ! _   = nothing 
    x ∷ xs ! zero = just x 
    x ∷ xs ! (suc n) = xs ! n 

infix 5 _!_ 

lookup : ∀ {A}{x : A}(xs : List A) → x ∈ xs → Σ ℕ (λ n → xs ! n ≡ just x) 

_,_ è un costruttore di due dipendenti, Σprojₗ rendimenti prima parte della coppia, _∈_ è un rapporto di appartenenza, lst ! i rendimenti just $(i-th element) se la lunghezza list s' è maggiore o uguale di i, nothing - altrimenti. Voglio scrivere una funzione lookup che accetta la lista xs, la prova di appartenenza x ∈ xs, e restituisce coppia dipendente di numero naturale e funzione che per numero naturale n restituisce prova (o smentita) del fatto che l'n-esimo elemento della lista è just x. Ora la funzione sembra

lookup : ∀ {A}{x : A}(xs : List A) → x ∈ xs → Σ ℕ (λ n → xs ! n ≣ just x) 
lookup {A} {x} .(x ∷ xs) (inHead {xs}) = 0 , refl 
lookup .(y ∷ xs) (inTail {y} {xs} proof) = (1 + Σprojₗ (lookup xs proof)) , ? 

Suppongo che avrei dovuto scrivere qualche funzione come Σprojᵣ (deve restituire secondo elemento della coppia, la funzione con la firma A → Set) per riempire il buco, ma non ho idea di come scriverlo . L'unica variante che è stata typechecked è

Σprojᵣ : {A : Set}{B : A → Set} → Σ A B → (A → Set) 
Σprojᵣ {A} {B} (a , b) = B 

, ma non mi è riuscito come finire lookup funzione con questo. Come posso risolvere questo esercizio?

Answer 1

In effetti, supponendo che Σprojᵣ progetti il ​​secondo elemento della coppia, Σprojᵣ (lookup xs proof) è la soluzione corretta che si inserisce nel foro. La domanda è, come scrivere questa proiezione?

---

se avessimo coppie non dipendenti ordinari, scrivendo entrambe le proiezioni è facile:

data _×_ (A B : Set) : Set where 
    _,′_ : A → B → A × B 

fst : ∀ {A B} → A × B → A 
fst (a ,′ b) = a 

snd : ∀ {A B} → A × B → B 
snd (a ,′ b) = b 

Ciò che lo rende così difficile quando usiamo coppia dipendente? Il suggerimento è nascosto nel nome stesso: il secondo componente dipende dal valore del primo e dobbiamo in qualche modo catturarlo nel nostro tipo.

Quindi, si parte con:

data Σ (A : Set) (B : A → Set) : Set where 
    _,_ : (a : A) → B a → Σ A B 

Scrivendo la proiezione per la componente di sinistra è facile (notare che io sto chiamando proj₁ invece di Σprojₗ, questo è ciò che la libreria standard fa):

proj₁ : {A : Set} {B : A → Set} → Σ A B → A 
proj₁ (a , b) = a 

Ora, il secondo di proiezione deve guardare un po 'come questo:

proj₂ : {A : Set} {B : A → Set} → Σ A B → B ? 
proj₂ (a , b) = b 

Ma Bcosa? Poiché il tipo del secondo componente dipende dal valore del primo, in qualche modo è necessario contraffarlo tramite B.

abbiamo bisogno di essere in grado di fare riferimento alla nostra coppia, facciamolo:

proj₂ : {A : Set} {B : A → Set} (pair : Σ A B) → B ? 

E ora, il primo componente della nostra coppia è proj₁ pair, quindi cerchiamo di riempimento che in:

proj₂ : {A : Set} {B : A → Set} (pair : Σ A B) → B (proj₁ pair) 

E in effetti, questo typechecks!

---

Esistono tuttavia soluzioni più semplici rispetto alla scrittura manuale di proj₂.

Invece di definire Σ come data, è possibile definirlo come record. I record sono casi speciali di dichiarazioni data che hanno un solo costruttore. La cosa bella è che i record si danno le proiezioni gratuitamente:

record Σ (A : Set) (B : A → Set) : Set where 
    constructor _,_ 
    field 
    proj₁ : A 
    proj₂ : B proj₁ 

open Σ -- opens the implicit record module 

Questo (tra le altre cose utili) ti dà proiezioni proj₁ e proj₂.

---

Possiamo anche decostruire la coppia con with dichiarazione ed evitare questo proj bussiness del tutto:

lookup : ∀ {A} {x : A}(xs : List A) → x ∈ xs → Σ ℕ (λ n → xs ! n ≡ just x) 
lookup {x = x} .(x ∷ xs) (first {xs}) = 0 , refl 
lookup   .(y ∷ xs) (later {y} {xs} p) with lookup xs p 
... | n , p′ = suc n , p′ 

with si permette di pattern matching, non solo sugli argomenti della funzione, ma anche sulle espressioni intermedie . Se hai familiarità con Haskell, è qualcosa come un case.

---

Ora, questa è la soluzione quasi ideale, ma può comunque essere migliorata un po '. Si noti che dobbiamo portare l'implicito {x}, {xs} e {y} nel campo di applicazione solo per poter scrivere il modello di punti. Gli schemi di punti non partecipano alla corrispondenza dei modelli, vengono utilizzati come asserzioni che questa particolare espressione è l'unica che si adatta.

Ad esempio, nella prima equazione, il modello di punto ci dice che l'elenco deve avere assomigliato a x ∷ xs - lo sappiamo perché il modello corrisponde alla prova. Dal momento che solo noi pattern match sulla prova, l'argomento lista è un po 'ridondante:

lookup : ∀ {A} {x : A} (xs : List A) → x ∈ xs → Σ ℕ (λ n → xs ! n ≡ just x) 
lookup ._ first = 0 , refl 
lookup ._ (later p) with lookup _ p 
... | n , p′ = suc n , p′ 

Il compilatore può anche dedurre l'argomento per la chiamata ricorsiva! Se il compilatore riesce a capire queste cose da solo, siamo in grado di segnare in modo sicuro è implicita:

lookup : ∀ {A} {x : A} {xs : List A} → x ∈ xs → Σ ℕ (λ n → xs ! n ≡ just x) 
lookup first = 0 , refl 
lookup (later p) with lookup p 
... | n , p′ = suc n , p′ 

Ora, il passo finale: cerchiamo di portare in qualche astrazione. La seconda equazione separa la coppia, applica alcune funzioni (suc) e ricostruisce la coppia - abbiamo funzioni della mappa sulla coppia!

Ora, il tipo completamente dipendente per map è piuttosto complicato. Non scoraggiarti se non capisci! Quando tornerai con più conoscenze in seguito, lo troverai affascinante.

map : {A C : Set} {B : A → Set} {D : C → Set} 
     (f : A → C) (g : ∀ {a} → B a → D (f a)) → 
     Σ A B → Σ C D 
map f g (a , b) = f a , g b 

Confronta con:

map′ : {A B C D : Set} 
     (f : A → C) (g : B → D) → 
     A × B → C × D 
map′ f g (a ,′ b) = f a ,′ g b 

E concludiamo con il molto conciso:

lookup : ∀ {A} {x : A} {xs : List A} → x ∈ xs → Σ ℕ (λ n → xs ! n ≡ just x) 
lookup first  = 0 , refl 
lookup (later p) = map suc id (lookup p) 

Cioè, abbiamo map suc il primo componente e lasciare la seconda invariato (id).