为什么我们需要容器？
（借口：标题模仿我们为什么需要单子的标题？ ）
有容器 （和索引的）（和异教的）和描述 。 但是容器是有问题的 ，对于我的小规模的经验来说，容器的思考比描述的要难。 非索引容器的types与Σ同构 – 这是非常不确定的。 形状和位置的描述有助于，但在英寸
⟦_⟧ᶜ : ∀ {α β γ} -> Container α β -> Set γ -> Set (α ⊔ β ⊔ γ) ⟦ Sh ◃ Pos ⟧ᶜ A = ∃ λ sh -> Pos sh -> A Kᶜ : ∀ {α β} -> Set α -> Container α β Kᶜ A = A ◃ const (Lift ⊥)
我们基本上使用Σ而不是形状和位置。
容器上严格正向的自由单体的types有一个相当直接的定义，但是对于我来说， Freer单体的types看起来更简单（从某种意义上说， Freer单体甚至比文章中描述的平常Free单体更好）。
那么，我们能用比描述或其他东西更好的方式来处理容器呢？
在我看来，容器的价值（如容器理论）是它们的一致性 。 这种一致性使得可以使用容器表示作为可执行规范的基础，甚至可能是机器辅助的程序派生。
容器：理论工具，而不是一个很好的运行时数据表示策略
我不会推荐（标准化）容器的固定点作为实现recursion数据结构的一个很好的通用方法。 也就是说，知道一个给定的函子具有（最多为iso）作为一个容器的表示是有帮助的，因为它告诉你通用的容器function（很容易实现，一次完成，由于统一性）可以被实例化到你特定的函数，以及你应该期待什么样的行为。 但是，这并不是说容器的实施将以任何实际的方式是有效的。 事实上，我通常更喜欢一阶数据的一阶编码（标签和元组，而不是函数）。
为了解决术语问题，让我们说容器的typesCont （在Set ，但是其他的类别是可用的）由一个构造函数给出<| 包装两个领域，形状和职位
S : Set P : S -> Set
（这是用于确定西格玛types，Pitypes或Wtypes的数据的相同签名，但这并不意味着容器与这些事物中的任何一个相同，或者这些事物是相同的作为彼此）。
作为一个函子的这种事情的解释是由
[_]C : Cont -> Set -> Set [ S <| P ]CX = Sg S \ s -> P s -> X -- I'd prefer (s : S) * (P s -> X) mapC : (C : Cont){XY : Set} -> (X -> Y) -> [ C ]CX -> [ C ]CY mapC (S <| P) f (s , k) = (s , fok) -- o is composition
我们已经赢了 这是一次全部实施的map 。 更重要的是，函数法则是通过计算来保持的。 不需要对types的结构进行recursion来构build操作，也不需要对法律进行certificate。
描述是非规范化的容器
没有人试图声称，在操作上， Nat <| Fin Nat <| Fin提供了一个有效的列表实现，只是通过这个标识我们学习了一些有用的列表结构。
让我说说描述的东西。 为了读者的利益，让我重build它们。
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中的值描述其固定点提供数据types的函子。 他们描述哪些函数？
[_]D : Desc -> Set -> Set [ var ]DX = X [ sg AD ]DX = Sg A \ a -> [ D a ]DX [ pi AD ]DX = (a : A) -> [ D a ]DX [ one ]DX = One [ D * D' ]DX = Sg ([ D ]DX) \ _ -> [ D' ]DX mapD : (D : Desc){XY : Set} -> (X -> Y) -> [ D ]DX -> [ D ]DY mapD var fx = fx mapD (sg AD) f (a , d) = (a , mapD (D a) fd) mapD (pi AD) fg = \ a -> mapD (D a) f (ga) mapD one f <> = <> mapD (D * D') f (d , d') = (mapD D fd , mapD D' f d')
我们不可避免地要通过描述来recursion工作，所以这很难。 函数法也不是免费的。 在操作上，我们得到了更好的数据表示，因为当具体元组将要做时，我们不需要求助于函数编码。 但是我们必须更加努力地写程序。
请注意，每个容器都有一个说明：
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 AD) (a , d) = PosD (D a) d PosD (pi AD) f = Sg A \ a -> PosD (D a) (fa) PosD one <> = Zero PosD (D * D') (d , d') = PosD D d + PosD D' d' ContD : Desc -> Cont ContD D = ShD D <| PosD D
也就是说，容器是描述的一种正常forms。 这是一个练习，表明[ D ]DX自然同构于[ ContD D ]CX 。 这使生活变得更容易，因为说出要做什么来描述，从原则上来说，应该怎样去做正常forms的容器。 上述mapD操作原则上可以通过将同构融合到mapC的统一定义来mapC 。
差分结构：容器显示方式
同样，如果我们有一个平等的概念，我们可以说统一容器的单一上下文是什么
_-[_] : (X : Set) -> X -> Set X -[ x ] = Sg X \ x' -> (x == x') -> Zero dC : Cont -> Cont dC (S <| P) = (Sg SP) <| (\ { (s , p) -> P s -[ p ] })
也就是说，容器中的单孔上下文的形状是原始容器的形状和孔的位置的对; 这些位置是与孔的位置不同的原始位置。 在区分幂级数时，这就是“乘以指数，递减指数”的certificate相关版本。
这种统一的处理方式给了我们规范，从中我们可以推导出数百年的程序来计算多项式的导数。
dD : Desc -> Desc dD var = one dD (sg AD) = sg A \ a -> dD (D a) dD (pi AD) = 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')
我如何检查我的派生操作员的描述是否正确？ 通过检查它与容器的衍生物！
不要陷入这样的思想陷阱，只是因为一些想法的expression不是在操作上有帮助，它不能在概念上有帮助。
在“自由”monad
最后一件事。 Freer技巧等同于以一种特定的方式重新排列一个任意函数（转换到Haskell）
data Obfuncscate fx where (:<) :: forall p. fp -> (p -> x) -> Obfuncscate fx
但这不是容器的替代品 。 这是一个容器演示文稿的微调。 如果我们有强大的存在和依赖types，我们可以写
data Obfuncscate fx where (:<) :: pi (s :: exists p. fp) -> (fst s -> x) -> Obfuncscate fx
所以(exists p. fp)表示形状（在这里你可以select你的位置表示，然后用它的位置标记每个位置）， fst从形状（你select的位置表示）中挑选出存在的证人。 由于是集装箱展示，因此具有明显的严格肯定的优点。
在Haskell中，当然，你必须挖掘存在体，幸运的是只留下依赖于types的投影。 这是存在主义的弱点，certificate了这个等价的Obfuncscate f和f 。 如果你在具有强大存在的依赖型理论中尝试相同的技巧，那么编码会失去其独特性，因为你可以投影和区分不同的位置表示select。 也就是说，我可以代表Just 3
Just () :< const 3
或通过
Just True :< \ b -> if b then 3 else 5
而在Coq中，比如说，这些可能是明显不同的。
挑战：表征多态function
容器types之间的每个多态函数都是以特定的方式给出的。 有一致性工作，再次澄清我们的理解。
如果你有一些
f : {X : Set} -> [ S <| T ]CX -> [ S' <| T' ]CX
它由下面的数据（延伸地）给出，其中没有提及任何元素：
toS : S -> S' fromP : (s : S) -> P' (toS s) -> P s f (s , k) = (toS s , ko fromP s)
也就是说，在容器之间定义多态函数的唯一方法就是说如何将input形状转换为输出形状，然后说出如何从input位置填充输出位置。
对于严格正函数的首选表示，可以对多态函数进行类似的严格表征，从而消除对元素types的抽象。 （为了便于描述，我将使用它们的可缩放性来容器。）
挑战：捕捉“可移植性”
给定两个函子f和g ，很容易说出它们的成分是fog ：（ (fog) x把f (gx)东西包裹起来，给我们提供了“ g结构的f结构”。 但是你是否可以很容易地强加这样一个额外的条件，即所有存储在f结构中的f结构都具有相同的形状？
假设f >< g捕捉fog的转座片段，其中所有的g形状都是相同的，所以我们也可以把它转变成f结构的g结构。 例如，虽然[] o []给出了不规则的列表清单， [] >< []给出矩形matrix; [] >< Maybe给列表，这些列表不是全部就是全部。
给予><你的首选代表严格正函子。 对于容器来说，这很简单。
(S <| P) >< (S' <| P') = (S * S') <| \ { (s , s') -> P s * P' s' }
结论
集装箱以标准化的Sigma-then-Piforms，并不是一个有效的机器数据表示。 但是，一个给定的函子实现的知识，然而，作为一个容器的演示有助于我们理解其结构，并给它有用的设备。 许多有用的结构可以抽象地给容器，一旦所有的容器都必须按照其他的介绍进行个案分析。 所以，是的，学习容器是一个好主意，只要掌握实际执行的更具体的结构的基本原理。
