在我看来，容器的价值（如容器理论）在于它们均匀性。这种一致性为使用容器表示作为可执行规范甚至机器辅助程序推导的基础提供了相当大的范围。
容器：一个理论工具，不是一个好的运行时数据表示策略
I would not推荐（标准化）容器的固定点作为实现递归数据结构的良好通用方法。也就是说，知道给定函子具有（高达 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 ] })
也就是说，容器中单孔上下文的形状是原始容器的形状和孔的位置的对；这些位置是除孔位置之外的原始位置。这是幂级数微分时“乘以索引，递减索引”的证明相关版本。
这种统一的处理方式为我们提供了规范，我们可以从中导出数百年历史的程序来计算多项式的导数。
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技巧相当于以特定方式重新排列任意函子（切换到 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
so that (exists p. f p)代表形状（您可以在其中选择位置的表示，然后用其位置标记每个位置），以及fst从形状（您选择的位置表示）中挑选出存在见证。它的优点是明显严格正exactly因为它是一个容器演示。
当然，在 Haskell 中，你必须柯里化存在主义，幸运的是，这仅留下对类型投影的依赖。正是存在主义的弱点证明了Obfuncscate f and f。如果您在具有强存在性的依赖类型理论中尝试相同的技巧，编码就会失去其唯一性，因为您可以预测并区分不同的位置表示选择。也就是说，我可以代表Just 3 by
Just () :< const 3
or by
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)
也就是说，在容器之间定义多态函数的唯一方法是说明如何将输入形状转换为输出形状，然后说明如何从输入位置填充输出位置。
对于严格正函子的首选表示，请给出多态函数的类似严格特征，从而消除对元素类型的抽象。 （对于描述，我将准确地使用它们对容器的可还原性。）
挑战：捕捉“可移植性”
给定两个函子，f and g，很容易说出它们的组成f o g is: (f o g) x将事物包裹起来f (g x)，给我们“f- 的结构g-结构”。但是你能轻易地强加一个额外的条件吗？g结构体存储在f结构具有相同的形状？
这么说吧f >< g捕捉到可转座的的片段f o g，其中所有的g形状是一样的，所以我们也可以把它变成一个g-结构f-结构。例如，同时[] o [] gives ragged列表的列表，[] >< [] gives 矩形的矩阵；[] >< Maybe给出全部列表Nothing or all Just.
Give ><为您首选的严格正函子表示。对于容器来说，就是这么简单。
(S <| P) >< (S' <| P') = (S * S') <| \ { (s , s') -> P s * P' s' }
结论
容器，以其标准化的 Sigma-then-Pi 形式，并不是为了成为数据的有效机器表示。但是，知道给定函子（实现）具有作为容器的表示形式，有助于我们理解其结构并为其提供有用的设备。当必须针对其他演示文稿逐一给出容器时，可以一次性为容器抽象地给出许多有用的构造。因此，是的，了解容器是一个好主意，即使只是为了掌握您实际实现的更具体结构背后的基本原理。
