在Agda中使用依赖对的问题

Question

我正在通过教程学习Agda,现在我正在阅读依赖对.

所以,这是代码片段:

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的长度大于i或等于,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?(它应该返回pair的第二个元素,带签名的函数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

当我们使用依赖对时,是什么让它变得如此困难？提示隐藏在名称中:第二个组件取决于first的值,我们必须以某种方式在我们的类型中捕获它.

所以,我们从:

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?手工书写更容易的解决方案.

我们可以将其定义?为a 而不是data定义为a 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- 我们知道这是因为我们在证明上匹配模式.由于我们只对证明进行模式匹配,因此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? = 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).