Lists: 列表与高阶函数
module plfa.part1.Lists where
本章节讨论列表（List）数据类型。我们用列表作为例子，来使用我们之前学习的技巧。同时， 列表也给我们带来多态类型（Polymorphic Types）和高阶函数（Higher-order Functions）的例子。
导入
import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; sym; trans; cong) open Eq.≡-Reasoning open import Data.Bool using (Bool; true; false; T; _∧_; _∨_; not) open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n) open import Data.Nat.Properties using (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ; *-distribʳ-+) open import Relation.Nullary using (¬_; Dec; yes; no) open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩) open import Function using (_∘_) open import Level using (Level) open import plfa.part1.Isomorphism using (_≃_; _⇔_)
列表
Agda 中的列表如下定义：data List (A : Set) : Set where [] : List A _∷_ : A → List A → List A infixr 5 _∷_
我们来仔细研究这个定义。如果 A 是个集合，那么 List A 也是一个集合。接下来的两行告诉我们 [] （读作 nil）是一个类型为 A 的列表（通常被叫做空列表），_∷_（读作 cons，是 constructor 的简写）取一个类型为 A 的值，和一个类型为 List A 的值，返回一个类型为 List A 的值。_∷_ 运算符的优先级是 5，向右结合。
例如：
_ : List ℕ _ = 0 ∷ 1 ∷ 2 ∷ []
表示了一个三个自然数的列表。因为 _∷_ 向右结合，这一项被解析成 0 ∷ (1 ∷ (2 ∷ []))。 在这里，0 是列表的第一个元素，称之为头（Head），1 ∷ (2 ∷ []) 是剩下元素的列表， 称之为尾（Tail）。列表是一个奇怪的怪兽：它有一头一尾，中间没有东西，然而它的尾巴又是一个列表！
正如我们所见，参数化的类型可以被转换成索引类型。上面的定义与下列等价：
data List′ : Set → Set where []′ : ∀ {A : Set} → List′ A _∷′_ : ∀ {A : Set} → A → List′ A → List′ A
每个构造子将参数作为隐式参数。因此我们列表的例子也可以写作：
_ : List ℕ _ = _∷_ {ℕ} 0 (_∷_ {ℕ} 1 (_∷_ {ℕ} 2 ([] {ℕ})))
此处我们将隐式参数显式地声明。
包含下面的编译器指令
{-# BUILTIN LIST List #-}告诉 Agda，List 类型对应了 Haskell 的列表类型，构造子 [] 和 _∷_ 分别代表了 nil 和 cons，这可以让列表的表示更加的有效率。
列表语法
我们可以用下面的定义，更简便地表示列表：
pattern [_] z = z ∷ [] pattern [_,_] y z = y ∷ z ∷ [] pattern [_,_,_] x y z = x ∷ y ∷ z ∷ [] pattern [_,_,_,_] w x y z = w ∷ x ∷ y ∷ z ∷ [] pattern [_,_,_,_,_] v w x y z = v ∷ w ∷ x ∷ y ∷ z ∷ [] pattern [_,_,_,_,_,_] u v w x y z = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ []
这是我们第一次使用模式声明。举例来说，第三行告诉我们 [ x , y , z ] 等价于 x ∷ y ∷ z ∷ []。前者可以在模式或者等式的左手边，或者是等式右手边的项中出现。
附加
我们对于列表的第一个函数写作 _++_，读作附加（Append）：
infixr 5 _++_ _++_ : ∀ {A : Set} → List A → List A → List A [] ++ ys = ys (x ∷ xs) ++ ys = x ∷ (xs ++ ys)
A 类型是附加的隐式参数，这让这个函数变为一个多态（Polymorphic）函数 （即可以用作多种类型）。一个列表附加到空列表会得到该列表本身； 一个列表附加到非空列表所得到的列表，其头与附加到的非空列表相同，尾与所附加的列表相同。
我们举个例子，来展示将两个列表附加的计算过程：
_ : [ 0 , 1 , 2 ] ++ [ 3 , 4 ] ≡ [ 0 , 1 , 2 , 3 , 4 ] _ = begin 0 ∷ 1 ∷ 2 ∷ [] ++ 3 ∷ 4 ∷ [] ≡⟨⟩ 0 ∷ (1 ∷ 2 ∷ [] ++ 3 ∷ 4 ∷ []) ≡⟨⟩ 0 ∷ 1 ∷ (2 ∷ [] ++ 3 ∷ 4 ∷ []) ≡⟨⟩ 0 ∷ 1 ∷ 2 ∷ ([] ++ 3 ∷ 4 ∷ []) ≡⟨⟩ 0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [] ∎
附加两个列表需要对于第一个列表元素个数线性的时间。
论证附加
我们可以与用论证数几乎相同的方法来论证列表。下面是附加满足结合律的证明：++-assoc : ∀ {A : Set} (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs) ++-assoc [] ys zs = begin ([] ++ ys) ++ zs ≡⟨⟩ ys ++ zs ≡⟨⟩ [] ++ (ys ++ zs) ∎ ++-assoc (x ∷ xs) ys zs = begin (x ∷ xs ++ ys) ++ zs ≡⟨⟩ x ∷ (xs ++ ys) ++ zs ≡⟨⟩ x ∷ ((xs ++ ys) ++ zs) ≡⟨ cong (x ∷_) (++-assoc xs ys zs) ⟩ x ∷ (xs ++ (ys ++ zs)) ≡⟨⟩ x ∷ xs ++ (ys ++ zs) ∎
证明对于第一个参数进行归纳。起始步骤将列表实例化为 []，由直接的运算可证。 归纳步骤将列表实例化为 x ∷ xs，由直接的运算配合归纳假设可证。 与往常一样，归纳假设由递归使用证明函数来表明，此处为 ++-assoc xs ys zs。
回忆到 Agda 支持片段。使用 cong (x ∷_) 可以将归纳假设：
(xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)提升至等式：
x ∷ ((xs ++ ys) ++ zs) ≡ x ∷ (xs ++ (ys ++ zs))即证明中所需。
我们也可以简单地证明 [] 是 _++_ 的左幺元和右幺元。 左幺元的证明从定义中即可得：
++-identityˡ : ∀ {A : Set} (xs : List A) → [] ++ xs ≡ xs ++-identityˡ xs = begin [] ++ xs ≡⟨⟩ xs ∎右幺元的证明可由简单的归纳得到：
++-identityʳ : ∀ {A : Set} (xs : List A) → xs ++ [] ≡ xs ++-identityʳ [] = begin [] ++ [] ≡⟨⟩ [] ∎ ++-identityʳ (x ∷ xs) = begin (x ∷ xs) ++ [] ≡⟨⟩ x ∷ (xs ++ []) ≡⟨ cong (x ∷_) (++-identityʳ xs) ⟩ x ∷ xs ∎
我们之后会了解到，这三条性质表明了 _++_ 和 [] 在列表上构成了一个幺半群（Monoid）。
长度
在下一个函数里，我们来寻找列表的长度：
length : ∀ {A : Set} → List A → ℕ length [] = zero length (x ∷ xs) = suc (length xs)
同样，它取一个隐式参数 A。 空列表的长度为零。非空列表的长度比其尾列表长度多一。
_ : length [ 0 , 1 , 2 ] ≡ 3 _ = begin length (0 ∷ 1 ∷ 2 ∷ []) ≡⟨⟩ suc (length (1 ∷ 2 ∷ [])) ≡⟨⟩ suc (suc (length (2 ∷ []))) ≡⟨⟩ suc (suc (suc (length {ℕ} []))) ≡⟨⟩ suc (suc (suc zero)) ∎
计算列表的长度需要关于列表元素个数线性的时间。
在倒数第二行中，我们不可以直接写 length []，而需要写 length {ℕ} []。 因为 [] 没有元素，Agda 没有足够的信息来推导其隐式参数。
论证长度
两个附加在一起的列表的长度是两列表长度之和：
length-++ : ∀ {A : Set} (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys length-++ {A} [] ys = begin length ([] ++ ys) ≡⟨⟩ length ys ≡⟨⟩ length {A} [] + length ys ∎ length-++ (x ∷ xs) ys = begin length ((x ∷ xs) ++ ys) ≡⟨⟩ suc (length (xs ++ ys)) ≡⟨ cong suc (length-++ xs ys) ⟩ suc (length xs + length ys) ≡⟨⟩ length (x ∷ xs) + length ys ∎
证明对于第一个参数进行归纳。起始步骤将列表实例化为 []，由直接的运算可证。 如同之前一样，Agda 无法推导 length 的隐式参数，所以我们必须显式地给出这个参数。 归纳步骤将列表实例化为 x ∷ xs，由直接的运算配合归纳假设可证。 与往常一样，归纳假设由递归使用证明函数来表明，此处为 length-++ xs ys， 由 cong suc 来提升。
反转
我们可以使用附加，来简单地构造一个函数来反转一个列表：reverse : ∀ {A : Set} → List A → List A reverse [] = [] reverse (x ∷ xs) = reverse xs ++ [ x ]
空列表的反转是空列表。 非空列表的反转是其头元素构成的单元列表附加至其尾列表反转之后的结果。
下面的例子展示了如何反转一个列表。_ : reverse [ 0 , 1 , 2 ] ≡ [ 2 , 1 , 0 ] _ = begin reverse (0 ∷ 1 ∷ 2 ∷ []) ≡⟨⟩ reverse (1 ∷ 2 ∷ []) ++ [ 0 ] ≡⟨⟩ (reverse (2 ∷ []) ++ [ 1 ]) ++ [ 0 ] ≡⟨⟩ ((reverse [] ++ [ 2 ]) ++ [ 1 ]) ++ [ 0 ] ≡⟨⟩ (([] ++ [ 2 ]) ++ [ 1 ]) ++ [ 0 ] ≡⟨⟩ (([] ++ 2 ∷ []) ++ 1 ∷ []) ++ 0 ∷ [] ≡⟨⟩ (2 ∷ [] ++ 1 ∷ []) ++ 0 ∷ [] ≡⟨⟩ 2 ∷ ([] ++ 1 ∷ []) ++ 0 ∷ [] ≡⟨⟩ (2 ∷ 1 ∷ []) ++ 0 ∷ [] ≡⟨⟩ 2 ∷ (1 ∷ [] ++ 0 ∷ []) ≡⟨⟩ 2 ∷ 1 ∷ ([] ++ 0 ∷ []) ≡⟨⟩ 2 ∷ 1 ∷ 0 ∷ [] ≡⟨⟩ [ 2 , 1 , 0 ] ∎
这样子反转一个列表需要列表长度二次的时间。这是因为反转一个长度为 n 的列表需要 将长度为 1、2 直到 n - 1 的列表附加起来，而附加两个列表需要第一个列表长度线性的时间， 因此加起来就需要 n * (n - 1) / 2 的时间。（我们将在本章节后部分验证这一结果）
练习 reverse-++-distrib（推荐）
证明一个列表附加到另外一个列表的反转即是反转后的第二个列表附加至反转后的第一个列表：
reverse (xs ++ ys) ≡ reverse ys ++ reverse xs-- Your code goes here
练习 reverse-involutive（推荐）
当一个函数应用两次后与恒等函数作用相同，那么这个函数是一个对合（Involution）。 证明反转是一个对合：
reverse (reverse xs) ≡ xs-- Your code goes here
更快地反转
上面的定义虽然论证起来方便，但是它比期望中的实现更低效，因为它的运行时间是关于列表长度的二次函数。 我们可以将反转进行推广，使用一个额外的参数：
shunt : ∀ {A : Set} → List A → List A → List A shunt [] ys = ys shunt (x ∷ xs) ys = shunt xs (x ∷ ys)
这个定义对于第一个参数进行递归。第二个参数会变_大_，但这样做没有问题，因为我们递归的参数 在变_小_。
转移（Shunt）与反转的关系如下：shunt-reverse : ∀ {A : Set} (xs ys : List A) → shunt xs ys ≡ reverse xs ++ ys shunt-reverse [] ys = begin shunt [] ys ≡⟨⟩ ys ≡⟨⟩ reverse [] ++ ys ∎ shunt-reverse (x ∷ xs) ys = begin shunt (x ∷ xs) ys ≡⟨⟩ shunt xs (x ∷ ys) ≡⟨ shunt-reverse xs (x ∷ ys) ⟩ reverse xs ++ (x ∷ ys) ≡⟨⟩ reverse xs ++ ([ x ] ++ ys) ≡⟨ sym (++-assoc (reverse xs) [ x ] ys) ⟩ (reverse xs ++ [ x ]) ++ ys ≡⟨⟩ reverse (x ∷ xs) ++ ys ∎
证明对于第一个参数进行归纳。起始步骤将列表实例化为 []，由直接的运算可证。 归纳步骤将列表实例化为 x ∷ xs，由归纳假设和附加的结合律可证。 当我们使用归纳假设时，第二个参数实际上变大了，但是这样做没有问题，因为我们归纳的参数变小了。
使用一个会在归纳或递归的参数变小时，变大的辅助参数来进行推广，是一个常用的技巧。 这个技巧在以后的证明中很有用。
在定义了推广的转移之后，我们可以将其特化，作为一个更高效的反转的定义：
reverse′ : ∀ {A : Set} → List A → List A reverse′ xs = shunt xs []
因为我们之前证明的引理，我们可以直接地证明两个定义是等价的：
reverses : ∀ {A : Set} (xs : List A) → reverse′ xs ≡ reverse xs reverses xs = begin reverse′ xs ≡⟨⟩ shunt xs [] ≡⟨ shunt-reverse xs [] ⟩ reverse xs ++ [] ≡⟨ ++-identityʳ (reverse xs) ⟩ reverse xs ∎
下面的例子展示了如何快速反转列表 [ 0 , 1 , 2 ]：
_ : reverse′ [ 0 , 1 , 2 ] ≡ [ 2 , 1 , 0 ] _ = begin reverse′ (0 ∷ 1 ∷ 2 ∷ []) ≡⟨⟩ shunt (0 ∷ 1 ∷ 2 ∷ []) [] ≡⟨⟩ shunt (1 ∷ 2 ∷ []) (0 ∷ []) ≡⟨⟩ shunt (2 ∷ []) (1 ∷ 0 ∷ []) ≡⟨⟩ shunt [] (2 ∷ 1 ∷ 0 ∷ []) ≡⟨⟩ 2 ∷ 1 ∷ 0 ∷ [] ∎
现在反转一个列表需要的时间与列表的长度线性相关。
映射
映射将一个函数应用于列表中的所有元素，生成一个对应的列表。 映射是一个高阶函数（Higher-Order Function）的例子，它取一个函数作为参数，返回一个函数作为结果：
map : ∀ {A B : Set} → (A → B) → List A → List B map f [] = [] map f (x ∷ xs) = f x ∷ map f xs
空列表的映射是空列表。 非空列表的映射生成一个列表，其头元素是原列表的头元素在应用函数之后的结果， 其尾列表是原列表的尾列表映射后的结果。
下面的例子展示了如何使用映射来增加列表中的每一个元素：
_ : map suc [ 0 , 1 , 2 ] ≡ [ 1 , 2 , 3 ] _ = begin map suc (0 ∷ 1 ∷ 2 ∷ []) ≡⟨⟩ suc 0 ∷ map suc (1 ∷ 2 ∷ []) ≡⟨⟩ suc 0 ∷ suc 1 ∷ map suc (2 ∷ []) ≡⟨⟩ suc 0 ∷ suc 1 ∷ suc 2 ∷ map suc [] ≡⟨⟩ suc 0 ∷ suc 1 ∷ suc 2 ∷ [] ≡⟨⟩ 1 ∷ 2 ∷ 3 ∷ [] ∎
映射需要关于列表长度线性的时间。
我们常常可以利用柯里化，将映射作用于一个函数，获得另一个函数，然后在之后的时候应用获得的函数：
sucs : List ℕ → List ℕ sucs = map suc _ : sucs [ 0 , 1 , 2 ] ≡ [ 1 , 2 , 3 ] _ = begin sucs [ 0 , 1 , 2 ] ≡⟨⟩ map suc [ 0 , 1 , 2 ] ≡⟨⟩ [ 1 , 2 , 3 ] ∎
对于由另外一个类型参数化的类型，例如列表，常常有对应的映射，其接受一个函数，并返回另一个 从由给定函数定义域参数化的类型，到由给定函数值域参数化的函数。除此之外，一个对于 n 个类型 参数化的类型常常会有一个对于 n 个函数参数化的映射。
练习 map-compose（实践）
证明函数组合的映射是两个映射的组合：
map (g ∘ f) ≡ map g ∘ map f证明的最后一步需要外延性。
-- 请将代码写在此处。
练习 map-++-distribute（实践）
证明下列关于映射与附加的关系：
map f (xs ++ ys) ≡ map f xs ++ map f ys-- 请将代码写在此处。
练习 map-Tree（实践）
定义一个树数据类型，其叶节点类型为 A，内部节点类型为 B：
data Tree (A B : Set) : Set where leaf : A → Tree A B node : Tree A B → B → Tree A B → Tree A B
定义一个对于树的映射运算符：
map-Tree : ∀ {A B C D : Set} → (A → C) → (B → D) → Tree A B → Tree C D-- 请将代码写在此处。
折叠
折叠取一个运算符和一个值，并使用运算符将列表中的元素合并至一个值，如果给定的列表为空， 则使用给定的值：
foldr : ∀ {A B : Set} → (A → B → B) → B → List A → B foldr _⊗_ e [] = e foldr _⊗_ e (x ∷ xs) = x ⊗ foldr _⊗_ e xs
空列表的折叠是给定的值。 非空列表的折叠使用给定的运算符，将头元素和尾列表的折叠合并起来。
下面的例子展示了如何使用折叠来对一个列表求和：
_ : foldr _+_ 0 [ 1 , 2 , 3 , 4 ] ≡ 10 _ = begin foldr _+_ 0 (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) ≡⟨⟩ 1 + foldr _+_ 0 (2 ∷ 3 ∷ 4 ∷ []) ≡⟨⟩ 1 + (2 + foldr _+_ 0 (3 ∷ 4 ∷ [])) ≡⟨⟩ 1 + (2 + (3 + foldr _+_ 0 (4 ∷ []))) ≡⟨⟩ 1 + (2 + (3 + (4 + foldr _+_ 0 []))) ≡⟨⟩ 1 + (2 + (3 + (4 + 0))) ∎
折叠需要关于列表长度线性的时间。
我们常常可以利用柯里化，将折叠作用于一个运算符和一个值，获得另一个函数， 然后在之后的时候应用获得的函数：
sum : List ℕ → ℕ sum = foldr _+_ 0 _ : sum [ 1 , 2 , 3 , 4 ] ≡ 10 _ = begin sum [ 1 , 2 , 3 , 4 ] ≡⟨⟩ foldr _+_ 0 [ 1 , 2 , 3 , 4 ] ≡⟨⟩ 10 ∎
正如列表由两个构造子 [] 和 _∷_，折叠函数取两个参数 e 和 _⊗_ （除去列表参数）。推广来说，一个有 n 个构造子的数据类型，会有对应的 取 n 个参数的折叠函数。
举另外一个例子，观察
foldr _∷_ [] xs ≡ xs若 xs 的类型为 List A，那么我们就会有一个 foldr 的实例，其中的 A 为 A，而 B 为 List A。它遵循
xs ++ ys ≡ foldr _∷_ ys xs二者相等的证明留作练习。
练习 product （推荐）
使用折叠来定义一个计算列表数字之积的函数。例如：
product [ 1 , 2 , 3 , 4 ] ≡ 24-- 请将代码写在此处。
练习 foldr-++ （推荐）
证明折叠和附加有如下的关系：
foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs-- 请将代码写在此处。
Exercise foldr-∷ (practice)
Show
foldr _∷_ [] xs ≡ xsShow as a consequence of foldr-++ above that
xs ++ ys ≡ foldr _∷_ ys xs练习 map-is-foldr
证明映射可以用折叠定义：
-- 请将代码写在此处。
此证明需要外延性。
练习 map-is-foldr（实践）
请证明 map 可使用 fold 来定义：
map f ≡ foldr (λ x xs → f x ∷ xs) []此证明需要外延性。
-- 请将代码写在此处。
练习 fold-Tree（实践）
请为预先给定的三个类型定义一个合适的折叠函数：
fold-Tree : ∀ {A B C : Set} → (A → C) → (C → B → C → C) → Tree A B → C-- 请将代码写在此处。
练习 map-is-fold-Tree（实践）
对于树数据类型，证明与 map-is-foldr 相似的性质。
-- 请将代码写在此处。
证明 sum-downFrom （延伸）
定义一个向下数数的函数：
downFrom : ℕ → List ℕ downFrom zero = [] downFrom (suc n) = n ∷ downFrom n
例如：
_ : downFrom 3 ≡ [ 2 , 1 , 0 ] _ = refl
证明数列之和 (n - 1) + ⋯ + 0 等于 n * (n ∸ 1) / 2：
sum (downFrom n) * 2 ≡ n * (n ∸ 1)-- 请将代码写在此处。
幺半群
一般来说，我们会对于折叠函数使用一个满足结合律的运算符，和这个运算符的左右幺元。 这意味着这个运算符和这个值形成了一个幺半群。
我们可以用一个合适的记录类型来定义幺半群：
record IsMonoid {A : Set} (_⊗_ : A → A → A) (e : A) : Set where field assoc : ∀ (x y z : A) → (x ⊗ y) ⊗ z ≡ x ⊗ (y ⊗ z) identityˡ : ∀ (x : A) → e ⊗ x ≡ x identityʳ : ∀ (x : A) → x ⊗ e ≡ x open IsMonoid
举例来说，加法和零，乘法和一，附加和空列表，都是幺半群：
+-monoid : IsMonoid _+_ 0 +-monoid = record { assoc = +-assoc ; identityˡ = +-identityˡ ; identityʳ = +-identityʳ } *-monoid : IsMonoid _*_ 1 *-monoid = record { assoc = *-assoc ; identityˡ = *-identityˡ ; identityʳ = *-identityʳ } ++-monoid : ∀ {A : Set} → IsMonoid {List A} _++_ [] ++-monoid = record { assoc = ++-assoc ; identityˡ = ++-identityˡ ; identityʳ = ++-identityʳ }
如果 _⊗_ 和 e 构成一个幺半群，那么我们可以用相同的运算符和一个任意的值来表示折叠：
foldr-monoid : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e → ∀ (xs : List A) (y : A) → foldr _⊗_ y xs ≡ foldr _⊗_ e xs ⊗ y foldr-monoid _⊗_ e ⊗-monoid [] y = begin foldr _⊗_ y [] ≡⟨⟩ y ≡⟨ sym (identityˡ ⊗-monoid y) ⟩ (e ⊗ y) ≡⟨⟩ foldr _⊗_ e [] ⊗ y ∎ foldr-monoid _⊗_ e ⊗-monoid (x ∷ xs) y = begin foldr _⊗_ y (x ∷ xs) ≡⟨⟩ x ⊗ (foldr _⊗_ y xs) ≡⟨ cong (x ⊗_) (foldr-monoid _⊗_ e ⊗-monoid xs y) ⟩ x ⊗ (foldr _⊗_ e xs ⊗ y) ≡⟨ sym (assoc ⊗-monoid x (foldr _⊗_ e xs) y) ⟩ (x ⊗ foldr _⊗_ e xs) ⊗ y ≡⟨⟩ foldr _⊗_ e (x ∷ xs) ⊗ y ∎
在之前的练习中，我们证明了以下定理：
postulate foldr-++ : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) (xs ys : List A) → foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs
由此，我们可以将幺半群中附加的折叠如下分解成两个折叠：
foldr-monoid-++ : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e → ∀ (xs ys : List A) → foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ e xs ⊗ foldr _⊗_ e ys foldr-monoid-++ _⊗_ e monoid-⊗ xs ys = begin foldr _⊗_ e (xs ++ ys) ≡⟨ foldr-++ _⊗_ e xs ys ⟩ foldr _⊗_ (foldr _⊗_ e ys) xs ≡⟨ foldr-monoid _⊗_ e monoid-⊗ xs (foldr _⊗_ e ys) ⟩ foldr _⊗_ e xs ⊗ foldr _⊗_ e ys ∎
练习 foldl（实践）
定义一个函数 foldl，与 foldr 相似，但是运算符向左结合，而不是向右。例如：
foldr _⊗_ e [ x , y , z ] = x ⊗ (y ⊗ (z ⊗ e))
foldl _⊗_ e [ x , y , z ] = ((e ⊗ x) ⊗ y) ⊗ z-- 请将代码写在此处。
练习 foldr-monoid-foldl（实践）
证明如果 _⊗_ 和 e 构成幺半群，那么 foldr _⊗_ e 和 foldl _⊗_ e 的结果 永远是相同的。
-- 请将代码写在此处。
所有
我们也可以定义关于列表的谓词。最重要的两个谓词是 All 和 Any。
谓词 All P 当列表里的所有元素满足 P 时成立：
data All {A : Set} (P : A → Set) : List A → Set where [] : All P [] _∷_ : ∀ {x : A} {xs : List A} → P x → All P xs → All P (x ∷ xs)
这个类型有两个构造子，使用了与列表构造子相同的名称。第一个断言了 P 对于空列表的任何元素成立。 第二个断言了如果 P 对于列表的头元素和尾列表的所有元素成立，那么 P 对于这个列表的任何元素成立。 Agda 使用类型来区分构造子是用于构造一个列表，还是构造 All P 成立的证明。
比如说，All (_≤ 2) 对于一个每一个元素都小于等于二的列表成立。 回忆 z≤n 证明了对于任意 n， zero ≤ n 成立； 对于任意 m 和 n，如果 m≤n 证明了 m ≤ n，那么 s≤s m≤n 证明了 suc m ≤ suc n:
_ : All (_≤ 2) [ 0 , 1 , 2 ] _ = z≤n ∷ s≤s z≤n ∷ s≤s (s≤s z≤n) ∷ []
这里 _∷_ 和 [] 是 All P 的构造子，而不是 List A 的。 这三项分别是 0 ≤ 2、 1 ≤ 2 和 2 ≤ 2 的证明。
（读者可能会思考诸如 [_,_,_] 的模式是否可以用于构造 All 类型的值， 像构造 List 类型的一样，因为两者使用了相同的构造子。事实上这样做是可以的，只要两个类型 在模式声明时在作用域内。然而现在不是这样的情况，因为 List 先于 [_,_,_] 定义，而 All 在 之后定义。）
任意
谓词 Any P 当列表里的一些元素满足 P 时成立：
data Any {A : Set} (P : A → Set) : List A → Set where here : ∀ {x : A} {xs : List A} → P x → Any P (x ∷ xs) there : ∀ {x : A} {xs : List A} → Any P xs → Any P (x ∷ xs)
第一个构造子证明了列表的头元素满足 P，第二个构造子证明的列表的尾列表中的一些元素满足 P。 举例来说，我们可以如下定义列表的成员关系：
infix 4 _∈_ _∉_ _∈_ : ∀ {A : Set} (x : A) (xs : List A) → Set x ∈ xs = Any (x ≡_) xs _∉_ : ∀ {A : Set} (x : A) (xs : List A) → Set x ∉ xs = ¬ (x ∈ xs)
比如说，零是列表 [ 0 , 1 , 0 , 2 ] 中的一个元素。 我们可以用两种方法来展示这个事实，对应零在列表中出现了两次：第一个元素和第三个元素：
_ : 0 ∈ [ 0 , 1 , 0 , 2 ] _ = here refl _ : 0 ∈ [ 0 , 1 , 0 , 2 ] _ = there (there (here refl))
除此之外，我们可以展示三不在列表之中，因为任何它在列表中的证明会推导出矛盾：
not-in : 3 ∉ [ 0 , 1 , 0 , 2 ] not-in (here ()) not-in (there (here ())) not-in (there (there (here ()))) not-in (there (there (there (here ())))) not-in (there (there (there (there ()))))
() 出现了五次，分别表示没有 3 ≡ 0、 3 ≡ 1、 3 ≡ 0、 3 ≡ 2 和 3 ∈ [] 的证明。
所有和附加
一个谓词对两个附加在一起的列表的每个元素都成立，当且仅当这个谓词对两个列表的每个元素都成立：
All-++-⇔ : ∀ {A : Set} {P : A → Set} (xs ys : List A) → All P (xs ++ ys) ⇔ (All P xs × All P ys) All-++-⇔ xs ys = record { to = to xs ys ; from = from xs ys } where to : ∀ {A : Set} {P : A → Set} (xs ys : List A) → All P (xs ++ ys) → (All P xs × All P ys) to [] ys Pys = ⟨ [] , Pys ⟩ to (x ∷ xs) ys (Px ∷ Pxs++ys) with to xs ys Pxs++ys ... | ⟨ Pxs , Pys ⟩ = ⟨ Px ∷ Pxs , Pys ⟩ from : ∀ { A : Set} {P : A → Set} (xs ys : List A) → All P xs × All P ys → All P (xs ++ ys) from [] ys ⟨ [] , Pys ⟩ = Pys from (x ∷ xs) ys ⟨ Px ∷ Pxs , Pys ⟩ = Px ∷ from xs ys ⟨ Pxs , Pys ⟩
练习 Any-++-⇔ （推荐）
使用 Any 代替 All 与一个合适的 _×_ 的替代，证明一个类似于 All-++-⇔ 的结果。 作为结论，展示关联 _∈_ 和 _++_ 的一个等价关系。
-- 请将代码写在此处。
练习 All-++-≃ （延伸）
证明 All-++-⇔ 的等价关系可以被扩展至一个同构关系。
-- 请将代码写在此处。
练习 ¬Any⇔All¬（推荐）
请证明 Any 和 All 满足一个版本的德摩根定律：
(¬_ ∘ Any P) xs ⇔ All (¬_ ∘ P) xs（你能明白为什么这里的 _∘_ 被泛化到任意层级很重要吗？ 如全体多态一节所述。）
以下定律是否也成立？
(¬_ ∘ All P) xs ⇔ Any (¬_ ∘ P) xs若成立，请证明；否则请解释原因。
-- 请将代码写在此处。
练习 ¬Any≃All¬（拓展）
请证明等价的 ¬Any⇔All¬ 可以被扩展成一个同构。 你需要使用外延性。
-- 请将代码写在此处
练习 All-∀（实践）
请证明 All P xs 同构于 ∀ x → x ∈ xs → P x.
-- 请将代码写在此处
练习 Any-∃（实践）
请证明 Any P xs 同构于 ∃[ x ] (x ∈ xs × P x).
-- 请将代码写在此处
如果成立，请证明；如果不成立，请解释原因。
所有的可判定性
如果我们将一个谓词看作一个返回布尔值的函数，那么我们可以简单的定义一个类似于 All 的函数，其当给定谓词对于列表每个元素返回真时返回真：
all : ∀ {A : Set} → (A → Bool) → List A → Bool all p = foldr _∧_ true ∘ map p
我们可以使用高阶函数 map 和 foldr 来简洁地写出这个函数。
正如所希望的那样，如果我们将布尔值替换成可判定值，这与 All 是相似的。首先，回到将 P 当作一个类型为 A → Set 的函数的概念，将一个类型为 A 的值 x 转换成 P x 对 x 成立 的证明。我们成 P 为可判定的（Decidable），如果我们有一个函数，其在给定 x 时能够判定 P x：
Decidable : ∀ {A : Set} → (A → Set) → Set Decidable {A} P = ∀ (x : A) → Dec (P x)那么当谓词
P 可判定时，我们亦可判定列表中的每一个元素是否满足这个谓词：All? : ∀ {A : Set} {P : A → Set} → Decidable P → Decidable (All P) All? P? [] = yes [] All? P? (x ∷ xs) with P? x | All? P? xs ... | yes Px | yes Pxs = yes (Px ∷ Pxs) ... | no ¬Px | _ = no λ{ (Px ∷ Pxs) → ¬Px Px } ... | _ | no ¬Pxs = no λ{ (Px ∷ Pxs) → ¬Pxs Pxs }
如果列表为空，那么 P 显然对列表的每个元素成立。 否则，证明的结构与两个可判定的命题是可判定的证明相似，不过我们使用 _∷_ 而不是 ⟨_,_⟩ 来整合头元素和尾列表的证明。
练习 Any?（延伸）
正如 All 有类似的 all 和 All? 形式，来判断列表的每个元素是否满足给定的谓词， 那么 Any 也有类似的 any 和 Any? 形式，来判断列表的一些元素是否满足给定的谓词。 给出它们的定义。
-- 请将代码写在此处。
练习 split（延伸）
关系 merge 在两个列表合并的结果为给定的第三个列表时成立。
data merge {A : Set} : (xs ys zs : List A) → Set where [] : -------------- merge [] [] [] left-∷ : ∀ {x xs ys zs} → merge xs ys zs -------------------------- → merge (x ∷ xs) ys (x ∷ zs) right-∷ : ∀ {y xs ys zs} → merge xs ys zs -------------------------- → merge xs (y ∷ ys) (y ∷ zs)
例如
_ : merge [ 1 , 4 ] [ 2 , 3 ] [ 1 , 2 , 3 , 4 ] _ = left-∷ (right-∷ (right-∷ (left-∷ [])))
给定一个可判定谓词和一个列表，我们可以将该列表拆分成两个列表， 二者可以合并成原列表，其中一个列表的所有元素都满足该谓词， 而另一个列表中的所有元素都不满足该谓词。
在列表上定义一个传统 filter 函数的变体，如下所示，它接受一个可判定谓词 和一个列表，返回一个所有元素都满足该谓词的列表，和一个所有元素都不满足的列表， 以及与它们相应的证明。
split : ∀ {A : Set} {P : A → Set} (P? : Decidable P) (zs : List A)
→ ∃[ xs ] ∃[ ys ] ( merge xs ys zs × All P xs × All (¬_ ∘ P) ys )-- 请将代码写在此处
标准库
标准库中可以找到与本章节中相似的定义：
import Data.List using (List; _++_; length; reverse; map; foldr; downFrom) import Data.List.Relation.Unary.All using (All; []; _∷_) import Data.List.Relation.Unary.Any using (Any; here; there) import Data.List.Membership.Propositional using (_∈_) import Data.List.Properties using (reverse-++-commute; map-compose; map-++-commute; foldr-++) renaming (mapIsFold to map-is-foldr) import Algebra.Structures using (IsMonoid) import Relation.Unary using (Decidable) import Relation.Binary using (Decidable)
标准库中的 IsMonoid 与给出的定义不同，因为它可以针对特定的等价关系参数化。
Relation.Unary 和 Relation.Binary 都定义了 Decidable 的某个版本，一个 用于单元关系（正如本章中的单元谓词 P），一个用于二元关系（正如之前使用的 _≤_）。
Unicode
本章使用了下列 Unicode：
∷ U+2237 比例 (\::)
⊗ U+2297 带圈的乘号 (\otimes, \ox)
∈ U+2208 元素属于 (\in)
∉ U+2209 元素不属于 (\inn, \notin)