所以,这是代码片段：
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,则返回$(第i个元素),否则为no.我想要写的查找函数,它接受列表XS,会员的x∈XS的证明,并返回取决于对自然数和功能,其为自然数的n个返回的事实,即列表的第n个元素是证明(或反证)只是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
如果我们有普通的非依赖对,那么编写两个投影很容易：
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
当我们使用依赖对时,是什么让它变得如此困难？提示隐藏在名称中：第二个组件取决于first的值,我们必须以某种方式在我们的类型中捕获它.
所以,我们从：
data Σ (A : Set) (B : A → Set) : Set where _,_ : (a : A) → B a → Σ A B
编写左侧组件的投影很容易(请注意,我称之为proj 1而不是Σ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 1对,所以让我们填写：
proj₂ : {A : Set} {B : A → Set} (pair : Σ A B) → B (proj₁ pair)
事实上,这个样式！
但是,与手工编写proj 2相比,有更简单的解决方案.
我们可以将其定义为记录,而不是将Σ定义为数据.记录是只有一个构造函数的数据声明的特例.好消息是记录为您提供免费的预测：
record Σ (A : Set) (B : A → Set) : Set where
constructor _,_
field
proj₁ : A
proj₂ : B proj₁
open Σ -- opens the implicit record module
这个(以及其他有用的东西)给你投影proj 1和proj 2.
我们也可以用声明解构对,并完全避免这个项目：
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,它就像一个案例.
现在,这几乎是理想的解决方案,但仍然可以做得更好.请注意,我们必须将隐式{x},{xs}和{y}带入范围,以便我们可以记下点模式.点模式不参与模式匹配,它们被用作断言,这个特定的表达式是唯一适合的模式.
例如,在第一个等式中,点图案告诉我们列表必须看起来像x∷xs – 我们知道这是因为我们在证明上匹配模式.由于我们只对证明进行模式匹配,因此list参数有点多余：
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′
编译器甚至可以推断出递归调用的参数！如果编译器可以自己计算这些东西,我们可以安全地将其标记为隐式：
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)并重建该对 – 我们在该对上映射函数！
现在,地图的完全依赖类型非常复杂.如果你不明白,不要气馁！当你以后回来了解更多知识时,你会发现它很有吸引力.
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).