从另一个 Data.List.All 构建一个 Data.List.All答案

【问题标题】：Building a Data.List.All from another Data.List.All从另一个 Data.List.All 构建一个 Data.List.All
【发布时间】：2018-05-05 19:29:35
【问题描述】：

假设我有以下范围：

A : Set
xs = [x1, x2, ..., xn] : List A
f : A → Set

然后我可以使用Data.List.All 来创建一个包含y1 : f x1、y2 : f x2、...、yn : f xn 的类型：

ys = [y1, y2, ..., yn] : All f xs

我的问题是，假设我有另一个功能

g : {x : A} → f x → Set

标准库中有什么东西可以将其转换为AllAll g ys 类型，这样我就可以在某些zs = [z1, ..., zn] : AllAll g ys 中拥有z1 : g {x1} y1、z2 : g {x2} y2、...、zn : g {xn} yn？

为了澄清，这是我自己实现它的方法；我的问题是我是否必须这样做，或者我可以使用标准库中的某些内容（可能是Data.List.All 本身？）：

data AllAll {A : Set} {f : A → Set} (g : {x : A} → f x → Set) : {xs : List A} → (ys : All f xs) → Set where
  [] : AllAll g []
  _∷_ : ∀ {x y xs ys} → g y → AllAll g ys → AllAll g {x ∷ xs} (y ∷ ys)

【问题讨论】：

标签： list standard-library agda

【解决方案1】：

您确实可以为此使用现有的All。首先定义一个“忘记”All 结构的函数：

open import Data.List
open import Data.List.All
open import Data.Product

lower-All : ∀ {a p} {A : Set a} {P : A → Set p} {xs} → All P xs → List (∃ P)
lower-All [] = []
lower-All (x ∷ xs) = (_ , x) ∷ lower-All xs

然后简单地用All 本身组成这个函数：

AllAll : ∀ {a x p} {X : Set x} {A : X → Set a} (P : ∀ {x} → A x → Set p) 
        → ∀ {xs} → All A xs → Set _
AllAll P = λ xs → All (P ∘ proj₂) (lower-All xs)

这样做的一个缺点是，要在 ys : AllAll P xs 上进行模式匹配，您必须首先在 xs 上进行模式匹配。根据您需要在AllAll 上编写哪个模式匹配的函数数量，这种编码可能不是很方便。一个好处是您可以免费获得额外的“嵌套”：

AllAllAll : ∀ {l₀ l₁ l₂ l₃} 
   {A₀ : Set l₀}
   {A₁ : A₀ → Set l₁} 
   {A₂ : ∀ {x} → A₁ x → Set l₂}
   (A₃ : ∀ {x} {y : A₁ x} → A₂ y → Set l₃)
   → ∀ {xs₀} {xs₁ : All A₁ xs₀} (xs₂ : AllAll A₂ xs₁) → Set _
AllAllAll P = AllAll P

（虽然如果你发现自己需要这样一个怪物，也许可以考虑重构你的程序......）

我作为练习离开，以证明此版本与 OP 中的版本之间的同构。

【讨论】：