在我看来，容器的价值（就像在容器理论中一样）在于它们的“一致性”。这种一致性为使用容器表示作为可执行规范的基础提供了相当大的空间，甚至可能是机器辅助的程序派生。

容器：一个理论工具，而不是一个好的运行时数据表示策略

我 * 不 * 建议使用（规范化）容器作为实现递归数据结构的良好通用方式。也就是说，了解给定函子具有（直到iso）将演示文稿作为容器，因为它告诉您通用容器功能（由于一致性，这很容易一次性实现）可以示例化为特定的函子，和元组，而不是函数）的一阶数据的一阶编码。
为了修正术语，让我们假设容器的类型Cont（在Set上，但其他类别也可用）是由封装两个字段（形状和位置）的构造函数<|给出的

S : Set
P : S -> Set

(This是用于确定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

但这并不是容器的“替代”。这只是对容器表示形式的一点修饰。如果我们有“强”存在体和依赖类型，我们可以写

data Obfuncscate f x where
  (:<) :: pi (s :: exists p. f p) -> (fst s -> x) -> Obfuncscate f x

因此，(exists p. f p)表示形状（您可以选择位置表示，然后用位置标记每个位置），fst从形状（您选择的位置表示）中选择存在见证。它的优点是明显是严格肯定的 * 确切 *，因为它是容器表示。

当然，在Haskell中，你必须咖喱存在主义，幸运的是，它只依赖于类型投射。正是存在主义的弱点证明了Obfuncscate f和f的等价性。如果你在依赖类型理论中用强存在主义尝试同样的技巧，编码失去了它的唯一性，因为你可以投影和区分不同的位置表示选择。

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)

也就是说，在容器之间定义多态函数的唯一方法是说明如何将输入形状转换为输出形状，然后说明如何从输入位置填充输出位置。
对于严格正函子的首选表示，请给予多态函数的类似的严格特征描述，以消除对元素类型的抽象（对于描述，我将使用它们的可归约性）。

挑战：捕获“可转座性”

给定两个函子，f和g，很容易说出它们的复合f o g是什么：(f o g) x将内容封装在f (g x)中，给出了“g-结构的f-结构”。但是，您是否可以容易地施加额外的条件，即存储在f结构中的所有g结构都具有相同的形状？
假设f >< g捕获了f o g的 * 可转座 * 片段，其中所有的g形状都是相同的，因此我们也可以将其转化为f-结构的g-结构。例如，[] o []给出了 * 粗糙 * 的列表，而[] >< []给出了 * 矩形 * 矩阵; [] >< Maybe给出了全部为Nothing或全部为Just的列表。
给予><作为严格正函子的首选表示。对于容器，就这么简单。

(S <| P) >< (S' <| P') = (S * S') <| \ { (s , s') -> P s * P' s' }

结论
容器，以其规范化的Sigma-then-Pi形式，并不打算成为数据的有效机器表示。但是，一个给定的函子，无论如何实现，都有一个容器的表示，这一知识帮助我们理解它的结构，并为它提供有用的设备。许多有用的构造可以为容器抽象地给出，一劳永逸，当它们必须为其他表示逐个给出时。所以，是的，学习容器是一个好主意，即使只是为了掌握您实际实现的更具体的构造背后的基本原理。