Probleme mit der Verwendung von abhängigen Paaren in Agda

Question

Ich lerne Agda by tutorial, und jetzt lese ich über abhängige Paare.

Also, das ist das Code-Fragment:

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) 

_,_ ist ein Konstruktor abhängigen Paar, Σprojₗ kehrt ersten Teil des Paares ist _∈_ eine Beziehung der Mitgliedschaft, lst ! i kehrt just $(i-th element) wenn list ‚s Länge ist größer oder gleich wie ich, nothing - sonst. Ich möchte eine lookup Funktion schreiben, die Liste xs nimmt, Beweis der Mitgliedschaft x ∈ xs, und gibt abhängiges Paar natürliche Zahl und Funktion zurück, die für natürliche Zahl n Beweis (oder Widerlegung) der Tatsache zurückgibt, dass n-tes Element der Liste just x ist. Jetzt sieht die Funktion wie

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)) , ? 

Ich nehme an, dass ich eine Funktion schreiben sollte wie Σprojᵣ zum Füllen des Loches (es das zweite Element des Paares, Funktion mit Unterschrift A → Set zurückkehren sollte), aber ich habe keine Ahnung, wie es zu schreiben . Die einzige Variante, die typechecked wurde, ist

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

, aber ich habe es nicht geschafft, wie lookup Funktion mit diesem zu beenden. Wie löse ich diese Übung?

Answer 1

In der Tat, vorausgesetzt, dass Σprojᵣ projiziert das zweite Element des Paares, Σprojᵣ (lookup xs proof) ist die richtige Lösung, die in das Loch passt. Die Frage ist, wie man diese Projektion schreibt?

---

Wenn wir gewöhnliche nicht-abhängige Paare hatten, beide Projektionen zu schreiben ist einfach:

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 

Was es so schwierig macht, wenn wir abhängig Paar verwenden? Der Hinweis ist im Namen versteckt: Die zweite Komponente hängt vom Wert der ersten ab und wir müssen dies irgendwie in unserem Typ erfassen.

So beginnen wir mit:

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

die Projektion für das linke Komponente zu schreiben ist einfach (beachten Sie, dass ich es proj₁ statt Σprojₗ bin nennen, das ist, was die Standard-Bibliothek tut):

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

Nun sollte der zweite Vorsprung ein bisschen wie folgt aussehen:

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

Aber Bwas? Da der Typ der zweiten Komponente vom Wert der ersten abhängt, müssen wir ihn irgendwie durch B schmuggeln.

Wir müssen in der Lage, unsere Paar zu beziehen, machen wir es:

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

Und nun, die erste Komponente unseres Paares proj₁ pair, so lassen wir das ausfüllen:

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

Und tatsächlich, diese Typchecks!

---

Es gibt jedoch einfache Lösungen als proj₂ von Hand zu schreiben.

Anstatt Σ als data zu definieren, können wir es als record definieren. Datensätze sind Sonderfälle von data Deklarationen, die nur einen Konstruktor haben. Das Schöne daran ist, dass Datensätze, die Sie kostenlos die Projektionen geben:

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

open Σ -- opens the implicit record module 

Diese (unter anderem nützliche Dinge) Sie Projektionen proj₁ und proj₂ gibt.

---

Wir können auch das Paar mit with Aussage dekonstruieren und diese proj bussiness ganz vermeiden:

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 können Sie Muster Spiel nicht nur auf die Argumente der Funktion, sondern auch auf Zwischen Ausdrücke . Wenn Sie mit Haskell vertraut sind, ist es so etwas wie ein case.

---

Jetzt ist dies fast ideale Lösung, kann aber noch ein bisschen besser gemacht werden. Beachten Sie, dass wir die implizite {x}, {xs} und {y} in den Geltungsbereich bringen müssen, nur damit wir das Punktmuster aufschreiben können. Punktmuster nehmen nicht am Mustervergleich teil, sie werden als Assertionen verwendet, dass dieser bestimmte Ausdruck der einzige ist, der passt.

Zum Beispiel sagt uns das Punktmuster in der ersten Gleichung, dass die Liste wie x ∷ xs ausgesehen haben muss - wir wissen das, weil wir Muster auf dem Beweis gematcht haben. Da wir auf dem Beweis nur Muster übereinstimmen, ist die Liste Argument ein wenig redundant:

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′ 

Der Compiler kann auch das Argument in den rekursiven Aufruf schließen! Wenn die Compiler dieses Zeug auf seinem eigenen Figur, können wir sicher markieren implizit:

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′ 

nun der letzte Schritt: Lassen Sie sich in einem gewissen Abstraktion bringen. Die zweite Gleichung nimmt das Paar auseinander, wendet einige Funktionen an (suc) und rekonstruiert das Paar - wir Karte Funktionen über das Paar!

Jetzt ist der vollständig abhängige Typ für map ziemlich kompliziert. Sei nicht entmutigt, wenn du es nicht verstehst! Wenn Sie später mit mehr Wissen zurückkommen, werden Sie es faszinierend finden.

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 

Vergleichen mit:

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 

Und wir schließen, mit dem sehr prägnant:

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) 

Das heißt, wir suc über die erste Komponente abzubilden und die zweite unverändert (id verlassen).