为什么我们需要容器？
Why do we need containers?
（借口：标题模仿的标题）
有 containers (and indexed ones) (and hasochistic ones) and descriptions. But containers are problematic 并且根据我的非常小的经验，从容器的角度思考比从描述的角度思考更难。 non-indexed 容器的类型与 Σ 同构——这太不明确了。 shapes-and-positions 描述有帮助，但在
⟦_⟧ᶜ : ∀ {α β γ} -> Container α β -> Set γ -> Set (α ⊔ β ⊔ γ)
⟦ Sh ◃ Pos ⟧ᶜ A = ∃ λ sh -> Pos sh -> A
Kᶜ : ∀ {α β} -> Set α -> Container α β
Kᶜ A = A ◃ const (Lift ⊥)
我们基本上使用 Σ 而不是形状和位置。
strictly-positive 容器上的自由 monad 的类型有一个相当简单的定义，但是 Freer monad 的类型对我来说看起来更简单（并且在某种意义上 Freer monad 甚至比 Free monad 更好，如 paper).
中所述
那么我们可以用比描述或其他更好的方式来处理容器吗？
在我看来，容器的价值（在容器理论中）是它们的均匀性。这种一致性为使用容器表示作为可执行规范的基础提供了相当大的范围，甚至可能是机器辅助程序派生。
容器：一个理论工具，不是一个好的运行时间数据表示策略
我会不推荐（规范化）容器的固定点作为实现递归数据结构的良好通用方法。也就是说，知道给定的仿函数具有（最多 iso）作为容器的表示是有帮助的，因为它告诉您可以实例化通用容器功能（由于统一性，很容易实现，一劳永逸）对于您的特定仿函数，以及您应该期望的行为。但这并不是说容器实现在任何实际方面都是高效的。事实上，我通常更喜欢一阶数据的一阶编码（标签和元组，而不是函数）。
为了修正术语，假设容器的类型 Cont（在 Set 上，但其他类别可用）由构造函数 <| 给出，包含两个字段，形状和位置
S : Set
P : S -> Set
（这是用于确定 Sigma 类型、Pi 类型或 W 类型的相同数据签名，但这并不意味着容器与这些东西相同，或者这些东西彼此相同。）
函子的解释由
给出
[_]C : Cont -> Set -> Set
[ S <| P ]C X = Sg S \ s -> P s -> X -- I'd prefer (s : S) * (P s -> X)
mapC : (C : Cont){X Y : Set} -> (X -> Y) -> [ C ]C X -> [ C ]C Y
mapC (S <| P) f (s , k) = (s , f o k) -- o is composition
我们已经赢了。这是 map 一劳永逸的实施。更重要的是，函子定律仅通过计算就成立。不需要对类型的结构进行递归来构造运算，也不需要证明规律。
描述是非规范化容器
没有人试图声称，在操作上，Nat <| Fin 给出了列表的 高效 实现，只是通过进行这种识别，我们学到了一些关于列表结构的有用信息列出。
让我谈谈描述。为了懒惰的读者，我再重构一下。
data Desc : Set1 where
var : Desc
sg pi : (A : Set)(D : A -> Desc) -> Desc
one : Desc -- could be Pi with A = Zero
_*_ : Desc -> Desc -> Desc -- could be Pi with A = Bool
con : Set -> Desc -- constant descriptions as singleton tuples
con A = sg A \ _ -> one
_+_ : Desc -> Desc -> Desc -- disjoint sums by pairing with a tag
S + T = sg Two \ { true -> S ; false -> T }
Desc 中的值描述其定点给出数据类型的函子。他们描述了哪些仿函数？
[_]D : Desc -> Set -> Set
[ var ]D X = X
[ sg A D ]D X = Sg A \ a -> [ D a ]D X
[ pi A D ]D X = (a : A) -> [ D a ]D X
[ one ]D X = One
[ D * D' ]D X = Sg ([ D ]D X) \ _ -> [ D' ]D X
mapD : (D : Desc){X Y : Set} -> (X -> Y) -> [ D ]D X -> [ D ]D Y
mapD var f x = f x
mapD (sg A D) f (a , d) = (a , mapD (D a) f d)
mapD (pi A D) f g = \ a -> mapD (D a) f (g a)
mapD one f <> = <>
mapD (D * D') f (d , d') = (mapD D f d , mapD D' f d')
我们不可避免地必须通过递归来处理描述，所以这是一项更艰巨的工作。函子定律也不是免费的。我们在操作上获得了更好的数据表示，因为当具体元组可以执行时，我们不需要求助于功能编码。但是写程序还要更加努力
注意每个容器都有一个描述：
sg S \ s -> pi (P s) \ _ -> var
但每个描述都有一个表示作为同构容器也是事实。
ShD : Desc -> Set
ShD D = [ D ]D One
PosD : (D : Desc) -> ShD D -> Set
PosD var <> = One
PosD (sg A D) (a , d) = PosD (D a) d
PosD (pi A D) f = Sg A \ a -> PosD (D a) (f a)
PosD one <> = Zero
PosD (D * D') (d , d') = PosD D d + PosD D' d'
ContD : Desc -> Cont
ContD D = ShD D <| PosD D
也就是说，容器是描述的一种正常形式。这是一个证明 [ D ]D X 与 [ ContD D ]C X 自然同构的练习。这让生活变得更轻松，因为要说明如何处理描述，原则上只要说明如何处理它们的正常形式、容器就足够了。原则上，上述 mapD 操作可以通过将同构融合到 mapC.
的统一定义来获得
差异结构：容器指明方向
类似地，如果我们有一个平等的概念，我们可以说容器的单孔上下文是什么统一
_-[_] : (X : Set) -> X -> Set
X -[ x ] = Sg X \ x' -> (x == x') -> Zero
dC : Cont -> Cont
dC (S <| P) = (Sg S P) <| (\ { (s , p) -> P s -[ p ] })
即容器中单孔上下文的形状为原容器形状与孔位置的对；这些位置是除孔之外的原始位置。这是 "multiply by the index, decrement the index" 微分幂级数时的证明相关版本。
这种统一的处理方式为我们提供了规范，我们可以从中推导出具有数百年历史的程序来计算多项式的导数。
dD : Desc -> Desc
dD var = one
dD (sg A D) = sg A \ a -> dD (D a)
dD (pi A D) = sg A \ a -> (pi (A -[ a ]) \ { (a' , _) -> D a' }) * dD (D a)
dD one = con Zero
dD (D * D') = (dD D * D') + (D * dD D')
如何检查我的描述导数运算符是否正确？通过对照容器的导数检查它！
不要陷入这样的思维陷阱，即仅仅因为某些想法的呈现在操作上没有帮助，它在概念上就没有帮助。
关于 "Freer" 单子
最后一件事。 Freer 技巧相当于以特定方式重新排列任意函子（切换到 Haskell）
data Obfuncscate f x where
(:<) :: forall p. f p -> (p -> x) -> Obfuncscate f x
但这不是容器的替代品。这是容器展示的轻微柯里化。如果我们有 strong 存在和依赖类型，我们可以写
data Obfuncscate f x where
(:<) :: pi (s :: exists p. f p) -> (fst s -> x) -> Obfuncscate f x
所以(exists p. f p)代表形状（你可以选择你的位置表示，然后用它的位置标记每个地方），fst从形状（位置）中挑选出存在的见证您选择的表示形式）。它具有明显严格正向完全的优点，因为它是容器表示。
在 Haskell 中，当然，你必须 curry out the existential，幸运的是它只留下了对类型投影的依赖。正是存在主义的弱点证明了 Obfuncscate f 和 f 的等价性。如果您在具有强存在性的依赖类型理论中尝试相同的技巧，编码将失去其唯一性，因为您可以投射和区分位置的不同表示选择。也就是说，我可以用
表示Just 3
Just () :< const 3
或
Just True :< \ b -> if b then 3 else 5
比如说，在 Coq 中，这些可以证明是不同的。
挑战：表征多态函数
容器类型之间的每个多态函数都以特定方式给出。这种一致性再次澄清了我们的理解。
如果你有一些
f : {X : Set} -> [ S <| T ]C X -> [ S' <| T' ]C X
它（扩展地）由以下数据给出，其中没有提及任何元素：
toS : S -> S'
fromP : (s : S) -> P' (toS s) -> P s
f (s , k) = (toS s , k o fromP s)
也就是说，在容器之间定义多态函数的唯一方法是说如何将输入形状转换为输出形状，然后说如何从输入位置填充输出位置。
对于严格正函子的首选表示，请给出多态函数的类似严格表征，从而消除对元素类型的抽象。 （为了描述，我会使用它们对容器的可还原性。）
挑战：捕获"transposability"
给定两个函子，f 和 g，很容易说出它们的组成 f o g 是什么：(f o g) x 将东西包裹在 f (g x) 中，给我们“f-结构的g-结构”。但是你能轻易地施加额外的条件，即存储在 f 结构中的所有 g 结构具有相同的形状吗？
假设 f >< g 捕获 f o g 的 可转座 片段，其中所有 g 形状都相同，因此我们也可以将事物变成 g 结构的 f 结构。例如，虽然 [] o [] 给出了 ragged 列表列表，但 [] >< [] 给出了 rectangular 矩阵； [] >< Maybe 给出全部为 Nothing 或全部为 Just.
的列表
给出 >< 作为严格正函子的首选表示形式。对于容器，就这么简单。
(S <| P) >< (S' <| P') = (S * S') <| \ { (s , s') -> P s * P' s' }
结论
容器，以其规范化的 Sigma-then-Pi 形式，并非旨在成为数据的高效机器表示。但是，知道一个给定的仿函数，然而，实现了，有一个作为容器的表示，帮助我们理解它的结构并给它有用的设备。许多有用的构造可以为容器抽象地给出，一劳永逸，当它们必须逐个给出用于其他表示时。所以，是的，了解容器是个好主意，如果只是为了掌握您实际实施的更具体构造背后的基本原理。
（借口：标题模仿
有 containers (and indexed ones) (and hasochistic ones) and descriptions. But containers are problematic 并且根据我的非常小的经验，从容器的角度思考比从描述的角度思考更难。 non-indexed 容器的类型与 Σ 同构——这太不明确了。 shapes-and-positions 描述有帮助，但在
⟦_⟧ᶜ : ∀ {α β γ} -> Container α β -> Set γ -> Set (α ⊔ β ⊔ γ)
⟦ Sh ◃ Pos ⟧ᶜ A = ∃ λ sh -> Pos sh -> A
Kᶜ : ∀ {α β} -> Set α -> Container α β
Kᶜ A = A ◃ const (Lift ⊥)
我们基本上使用 Σ 而不是形状和位置。
strictly-positive 容器上的自由 monad 的类型有一个相当简单的定义，但是 Freer monad 的类型对我来说看起来更简单（并且在某种意义上 Freer monad 甚至比 Free monad 更好，如 paper).
那么我们可以用比描述或其他更好的方式来处理容器吗？
在我看来，容器的价值（在容器理论中）是它们的均匀性。这种一致性为使用容器表示作为可执行规范的基础提供了相当大的范围，甚至可能是机器辅助程序派生。
容器：一个理论工具，不是一个好的运行时间数据表示策略
我会不推荐（规范化）容器的固定点作为实现递归数据结构的良好通用方法。也就是说，知道给定的仿函数具有（最多 iso）作为容器的表示是有帮助的，因为它告诉您可以实例化通用容器功能（由于统一性，很容易实现，一劳永逸）对于您的特定仿函数，以及您应该期望的行为。但这并不是说容器实现在任何实际方面都是高效的。事实上，我通常更喜欢一阶数据的一阶编码（标签和元组，而不是函数）。
为了修正术语，假设容器的类型 Cont（在 Set 上，但其他类别可用）由构造函数 <| 给出，包含两个字段，形状和位置
S : Set
P : S -> Set
（这是用于确定 Sigma 类型、Pi 类型或 W 类型的相同数据签名，但这并不意味着容器与这些东西相同，或者这些东西彼此相同。）
函子的解释由
给出[_]C : Cont -> Set -> Set
[ S <| P ]C X = Sg S \ s -> P s -> X -- I'd prefer (s : S) * (P s -> X)
mapC : (C : Cont){X Y : Set} -> (X -> Y) -> [ C ]C X -> [ C ]C Y
mapC (S <| P) f (s , k) = (s , f o k) -- o is composition
我们已经赢了。这是 map 一劳永逸的实施。更重要的是，函子定律仅通过计算就成立。不需要对类型的结构进行递归来构造运算，也不需要证明规律。
描述是非规范化容器
没有人试图声称，在操作上，Nat <| Fin 给出了列表的 高效 实现，只是通过进行这种识别，我们学到了一些关于列表结构的有用信息列出。
让我谈谈描述。为了懒惰的读者，我再重构一下。
data Desc : Set1 where
var : Desc
sg pi : (A : Set)(D : A -> Desc) -> Desc
one : Desc -- could be Pi with A = Zero
_*_ : Desc -> Desc -> Desc -- could be Pi with A = Bool
con : Set -> Desc -- constant descriptions as singleton tuples
con A = sg A \ _ -> one
_+_ : Desc -> Desc -> Desc -- disjoint sums by pairing with a tag
S + T = sg Two \ { true -> S ; false -> T }
Desc 中的值描述其定点给出数据类型的函子。他们描述了哪些仿函数？
[_]D : Desc -> Set -> Set
[ var ]D X = X
[ sg A D ]D X = Sg A \ a -> [ D a ]D X
[ pi A D ]D X = (a : A) -> [ D a ]D X
[ one ]D X = One
[ D * D' ]D X = Sg ([ D ]D X) \ _ -> [ D' ]D X
mapD : (D : Desc){X Y : Set} -> (X -> Y) -> [ D ]D X -> [ D ]D Y
mapD var f x = f x
mapD (sg A D) f (a , d) = (a , mapD (D a) f d)
mapD (pi A D) f g = \ a -> mapD (D a) f (g a)
mapD one f <> = <>
mapD (D * D') f (d , d') = (mapD D f d , mapD D' f d')
我们不可避免地必须通过递归来处理描述，所以这是一项更艰巨的工作。函子定律也不是免费的。我们在操作上获得了更好的数据表示，因为当具体元组可以执行时，我们不需要求助于功能编码。但是写程序还要更加努力
注意每个容器都有一个描述：
sg S \ s -> pi (P s) \ _ -> var
但每个描述都有一个表示作为同构容器也是事实。
ShD : Desc -> Set
ShD D = [ D ]D One
PosD : (D : Desc) -> ShD D -> Set
PosD var <> = One
PosD (sg A D) (a , d) = PosD (D a) d
PosD (pi A D) f = Sg A \ a -> PosD (D a) (f a)
PosD one <> = Zero
PosD (D * D') (d , d') = PosD D d + PosD D' d'
ContD : Desc -> Cont
ContD D = ShD D <| PosD D
也就是说，容器是描述的一种正常形式。这是一个证明 [ D ]D X 与 [ ContD D ]C X 自然同构的练习。这让生活变得更轻松，因为要说明如何处理描述，原则上只要说明如何处理它们的正常形式、容器就足够了。原则上，上述 mapD 操作可以通过将同构融合到 mapC.
差异结构：容器指明方向
类似地，如果我们有一个平等的概念，我们可以说容器的单孔上下文是什么统一
_-[_] : (X : Set) -> X -> Set
X -[ x ] = Sg X \ x' -> (x == x') -> Zero
dC : Cont -> Cont
dC (S <| P) = (Sg S P) <| (\ { (s , p) -> P s -[ p ] })
即容器中单孔上下文的形状为原容器形状与孔位置的对；这些位置是除孔之外的原始位置。这是 "multiply by the index, decrement the index" 微分幂级数时的证明相关版本。
这种统一的处理方式为我们提供了规范，我们可以从中推导出具有数百年历史的程序来计算多项式的导数。
dD : Desc -> Desc
dD var = one
dD (sg A D) = sg A \ a -> dD (D a)
dD (pi A D) = sg A \ a -> (pi (A -[ a ]) \ { (a' , _) -> D a' }) * dD (D a)
dD one = con Zero
dD (D * D') = (dD D * D') + (D * dD D')
如何检查我的描述导数运算符是否正确？通过对照容器的导数检查它！
不要陷入这样的思维陷阱，即仅仅因为某些想法的呈现在操作上没有帮助，它在概念上就没有帮助。
关于 "Freer" 单子
最后一件事。 Freer 技巧相当于以特定方式重新排列任意函子（切换到 Haskell）
data Obfuncscate f x where
(:<) :: forall p. f p -> (p -> x) -> Obfuncscate f x
但这不是容器的替代品。这是容器展示的轻微柯里化。如果我们有 strong 存在和依赖类型，我们可以写
data Obfuncscate f x where
(:<) :: pi (s :: exists p. f p) -> (fst s -> x) -> Obfuncscate f x
所以(exists p. f p)代表形状（你可以选择你的位置表示，然后用它的位置标记每个地方），fst从形状（位置）中挑选出存在的见证您选择的表示形式）。它具有明显严格正向完全的优点，因为它是容器表示。
在 Haskell 中，当然，你必须 curry out the existential，幸运的是它只留下了对类型投影的依赖。正是存在主义的弱点证明了 Obfuncscate f 和 f 的等价性。如果您在具有强存在性的依赖类型理论中尝试相同的技巧，编码将失去其唯一性，因为您可以投射和区分位置的不同表示选择。也就是说，我可以用
Just 3
Just () :< const 3
或
Just True :< \ b -> if b then 3 else 5
比如说，在 Coq 中，这些可以证明是不同的。
挑战：表征多态函数
容器类型之间的每个多态函数都以特定方式给出。这种一致性再次澄清了我们的理解。
如果你有一些
f : {X : Set} -> [ S <| T ]C X -> [ S' <| T' ]C X
它（扩展地）由以下数据给出，其中没有提及任何元素：
toS : S -> S'
fromP : (s : S) -> P' (toS s) -> P s
f (s , k) = (toS s , k o fromP s)
也就是说，在容器之间定义多态函数的唯一方法是说如何将输入形状转换为输出形状，然后说如何从输入位置填充输出位置。
对于严格正函子的首选表示，请给出多态函数的类似严格表征，从而消除对元素类型的抽象。 （为了描述，我会使用它们对容器的可还原性。）
挑战：捕获"transposability"
给定两个函子，f 和 g，很容易说出它们的组成 f o g 是什么：(f o g) x 将东西包裹在 f (g x) 中，给我们“f-结构的g-结构”。但是你能轻易地施加额外的条件，即存储在 f 结构中的所有 g 结构具有相同的形状吗？
假设 f >< g 捕获 f o g 的 可转座 片段，其中所有 g 形状都相同，因此我们也可以将事物变成 g 结构的 f 结构。例如，虽然 [] o [] 给出了 ragged 列表列表，但 [] >< [] 给出了 rectangular 矩阵； [] >< Maybe 给出全部为 Nothing 或全部为 Just.
给出 >< 作为严格正函子的首选表示形式。对于容器，就这么简单。
(S <| P) >< (S' <| P') = (S * S') <| \ { (s , s') -> P s * P' s' }
结论
容器，以其规范化的 Sigma-then-Pi 形式，并非旨在成为数据的高效机器表示。但是，知道一个给定的仿函数，然而，实现了，有一个作为容器的表示，帮助我们理解它的结构并给它有用的设备。许多有用的构造可以为容器抽象地给出，一劳永逸，当它们必须逐个给出用于其他表示时。所以，是的，了解容器是个好主意，如果只是为了掌握您实际实施的更具体构造背后的基本原理。