代码之家 › 专栏 › 技术社区 › Cactus

构建数据。列表全部来自另一个数据。列表全部的

agda standard-library list

1

Cactus · 技术社区 · 7 年前

假设我的范围如下:

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 这样我就可以 z1 : g {x1} y1 , z2 : g {x2} y2 , ..., zn : g {xn} yn 在某些方面 zs = [z1, ..., zn] : AllAll g ys ?

澄清一下,以下是我自己将如何实施它;我的问题是我是否必须这样做,或者如果标准库中有什么东西(可能 数据列表全部的 本身?)我可以使用:

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)

1 回复 | 直到 7 年前

1

2

user2407038 7 年前

你确实可以使用现有的 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

然后简单地用 全部的 自身:

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中的版本之间的同构。