使用依賴對在Agda中的問題

Question

我在學習Agda by tutorial，現在我正在閱讀有關從屬對。

所以，這是代碼的片段：

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) 

_,_被依賴的對，Σprojₗ返回對第一部分，_∈_的構造函數成員的關係，lst ! i返回just $(i-th element)如果list的長度大於或等於我，nothing - 否則。我想寫一個lookup函數，其中包含列表xs，證明成員資格x ∈ xs，並且返回自然數n的自然數和函數的相關對返回列表的第n個元素爲just x的證明（或不可行）。現在函數看起來像

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

我想，我應該寫一些功能像Σprojᵣ用於填充孔（它應該返回對第二元素，簽名A → Set功能），但我不知道怎麼寫。這是typechecked唯一的變化是

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

，但我沒有管理如何完成lookup功能與此有關。我如何解決這個練習？

Answer 1

事實上，假設Σprojᵣ投射這一對中的第二個元素，Σprojᵣ (lookup xs proof)是適合該孔的正確解決方案。問題是，如何編寫這個預測？

---

如果我們有普通的非依賴對，寫兩個預測很簡單：

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 

是什麼讓這麼難，當我們使用依賴於對？提示隱藏在名字中：第二個組件取決於第一個的值，我們必須以某種方式捕獲這個類型。

那麼，我們就先從：

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

編寫投影左成分是容易的（請注意，我稱它proj₁而不是Σprojₗ，這是標準庫做什麼）：

現在

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

，第二投影應該有點像這樣：

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

但B什麼？由於第二個組件的類型取決於第一個組件的類型，因此我們需要通過B走私它。

我們需要能夠參考我們的對，讓我們做吧：

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

而現在，我們對的第一部分是proj₁ pair，讓我們填寫在：

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

事實上，這種類型！

---

然而，有比手寫proj₂更容易的解決方案。

而不是將Σ定義爲data，我們可以將其定義爲record。記錄是data聲明只有一個構造函數的特例。這種做法的好處是，記錄給你自由的預測：

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

open Σ -- opens the implicit record module 

這（以及其他有用的東西），讓你預測proj₁和proj₂。

---

我們還可以解構對與with語句，並完全避免這個proj經營業務：

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讓您模式匹配，不僅在功能上的爭論，也是對中間表達式。如果你對Haskell很熟悉，那就像case。現在

---

，這幾乎是理想的解決方案，但還是可以做出更好一點。請注意，我們必須將暗含的{x},{xs}和{y}納入範圍，以便我們可以記下點圖案。點模式不參與模式匹配，它們被用作斷言，該特定表達式是唯一適合的表達式。

例如，在第一個等式中，點陣模式告訴我們該列表必須看起來像x ∷ xs-我們知道這是因爲我們的模式匹配證明。因爲只有我們在檢驗模式匹配，列表的說法是有點多餘：

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′ 

編譯器甚至可以推斷出參數的遞歸調用！如果編譯器可以自行算出這個東西，我們可以放心地將其標記含蓄：

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′ 

現在，最後的步驟：讓我們在一些抽象帶來。第二個等式將這對分開，應用一些函數（suc）並重構對 - 我們地圖函數在這對中！

現在，map的完全依賴類型非常複雜。如果你不明白，不要氣餒！當你稍後回來瞭解更多知識時，你會發現它很有趣。

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 

比較：

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 

而且我們的結論與非常簡潔：

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) 

也就是說，我們映射suc在第一部分，並留下第二個不變（id ）。