为什么我们需要容器？ [英] Why do we need containers?
问题描述
有容器（和索引）（和 hasochistic ones）和说明。但容器存在问题，对于我非常小的体验，很难想象在容器方面而不是在描述方面。非索引容器的类型同构于Σ - 这是非常不确定的。形状和位置描述有帮助，但是在
⟦_⟧ᶜ：∀{αβγ} - >容器αβ->设置γ - > Set（α⊔β⊔γ）
⟦Sh◃Pos⟧ᶜA =∃λsh - > Pos sh - > A
Kᶜ：∀{αβ} - >设置α - >容器αβ
KᶜA =A◃常量（Lift⊥）
Σ而不是形状和位置。
容器上严格正向的自由单体的类型有一个相当直接的定义，但是 那么我们可以用比描述或其他东西更好的方式来处理容器？ 在我看来，容器的价值（如容器理论）是它们的均匀性。这种一致性使得使用容器表示法作为可执行规范的基础，甚至可能是机器辅助的程序派生。容器：理论工具，不是一个好的运行时间数据表示策略 我不推荐（标准化）容器的固定点作为实现递归数据结构的一种很好的通用方法。也就是说，知道给定的函子具有（最多为iso）作为容器的演示文件是有帮助的，因为它告诉您可以实例化通用容器功能（这很容易实现，一次完成，归功于均匀性）可以实例化到你特定的仿函数，以及你应该期望的行为。但这并不是说容器实现将以任何实际的方式高效。事实上，我通常更喜欢一阶数据的一阶编码（标签和元组，而不是函数）。 Freer monad的类型对我来说看起来更简单（从某种意义上讲， Freer monad甚至比平常更好 Free monad，详见论文
Cont 的容器（在 Set 中，但其他类别可用）由构造函数<< ; | 打包两个字段，形状和位置
S：设置
P：S - >设置
（这是用于确定Sigma类型或Pi的数据的相同签名类型或W类型，但这并不意味着容器与任何这些事物相同，或者这些事物彼此相同。）
作为仿函数的这种事物的解释由以下给出：
[_] C：Cont - >设置 - >设置
[S< | | P] C X = Sg S \\ s - > P s - > X - 我更喜欢（s：S）*（P s - > X）
mapC：（C：Cont）{X Y：Set} - > （X→Y）→> [C] C X - > [C] CY
mapC（S <| P）f（s，k）=（s，fok） - o是组合
我们已经赢了。这是 map 为所有人实施一次。更重要的是，函子法则仅通过计算就可以实现。没有必要对类型结构进行递归来构造操作或证明规律。
描述是非规格化容器
没有人试图声称，在操作上， Nat <| Fin 给出了一个高效的列表实现，只是通过这个标识我们学习了一些关于列表结构的有用信息。
让我说一些关于描述的内容。为了读者的利益，让我重新构建它们。
data描述：Set1其中
var：Desc
sg pi：（A：Set）（D：A - > Desc） - > Desc
one：Desc - 可以是Pi，A =零
_ * _：Desc - >说明 - > Desc - 可以是Pi，其中A = Bool
con：Set - > Desc - 作为单例元组的常量描述
con A = sg A \ _ - >一个
_ + _：Desc - >说明 - > Desc - 与标签配对的不相交和
S + T = sg Two \ {true - > S;错误 - > T
Desc 固定点提供数据类型。
[_] D：Desc - >设置 - > 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 = 1
[D * D'] D X = Sg（[D] D X）\ - > [D'] D X
mapD：（D：Desc）{X Y：Set} - > （X→Y）→> [D] D X - > [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（g a）
mapD one f<> =<>
mapD（D * D'）f（d，d'）=（mapD D fd，mapD D'f d'）
我们不可避免地要通过描述来递归工作，所以这很难。函数法也不是免费的。我们可以更好地表达数据，因为在具体元组完成时我们不需要诉诸功能编码。但我们必须更努力地编写程序。
请注意，每个容器都有一个说明：
sg S \\ s - > pi（P s）\ _ - > var
但是，每个描述都有一个演示文稿 容器。
ShD：Desc - > Set
ShD D = [D] D One
PosD：（D：Desc） - > ShD D - >设置
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<> =零
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 的统一定义来获得。 p>
差异结构：容器显示方式
同样，如果我们有一个平等的概念，我们可以说什么 -
_- [_]：（X：Set） - > X - > Set
X - [x] = Sg X \ x' - > （x == x'） - >零
dC：继续 - > 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 - > （D（D'））* dD（D a）
dD one = con Zero
dD（D * D '）=（dD D * D'）+（D * dD D'）
检查我的派生操作员的描述是否正确？通过检查它与容器的衍生物进行比较！
不要陷入这样的思维陷阱：仅仅因为某个想法的表达在概念上无法在操作上有帮助
在Freermonads
最后一件事。 Freer 技巧相当于以一种特定的方式重新排列一个任意的函子（切换到Haskell）。
data obfuncscate fx其中
（：<）:: forall p。 f p - > （p - > x） - > Obfuncscate f x
但这不是容器的替代选择。这是一个容器演示文稿的微调。如果我们有强大的存在和依赖类型，我们可以写成：
pre $ data数据obfuncscate fx其中
（：<）:: pi（s :: exists p。fp） - > （fst s - > x） - > Obfuncscate fx
让（存在p。fp）表示形状（在这里你可以选择你的位置表示，然后用它的位置标记每个位置），并且 fst 从形状中挑选存在证人（位置表示你选择了）。它具有明显的严格肯定的优点，因为它是一个容器演示文稿。
在Haskell中，当然，您必须将存在的，幸运的是只留下了依赖类型投影。这是存在主义的弱点，证明了 Obfuncscate f 和 f 的等价性。如果你在具有强大存在的依赖型理论中尝试相同的技巧，编码会失去其独特性，因为你可以投射和区分不同的位置表示选择。也就是说，我可以用 $ b
表示 Just 3 < const 3
或者
Just True：< \ b - >如果b然后是3 else 5
并且在Coq中，比如说，这些可以证明是不同的。
挑战：表征多态函数
容器类型之间的每个多态函数都以特定的方式给出。如果你有一些
<$ c $ c> f：{X：Set} - > [S< | T] C X - > [S'<| T'] CX
它由下面的数据给出（延伸），它们没有提到元素无论如何：
toS：S - > S'
fromP：（s：S） - > P'（toS s） - > P s
f（s，k）=（toS s，ko fromP s）
也就是说，在容器之间定义多态函数的唯一方法是说明如何将输入形状转换为输出形状，然后说出如何从输入位置填充输出位置。
对于严格正函数的首选表示，可以对多态函数进行类似的严格表征，从而消除对元素类型的抽象。 （关于描述，我将精确地将它们的可缩放性用于容器。）挑战：捕获可移植性
给定两个函数， f 和 g ，很容易说出它们的组成 fog 是：（雾）x 在 f（gx）中包装了一些东西， f - g -structures的结构。但是，您是否可以轻易施加额外的条件：存储在 f 结构中的所有 g 结构具有相同的形状？
假设 f>< g 捕获 fog 的转置段片段，其中所有 g 形状是相同的，所以我们可以把它变成一个 g - f 的结构。 -structures。例如， [] o [] 给出 列表的列表， []>< [] 给出矩形矩阵; []><也许给出的列表可能都是 Nothing 或全部 Just 。
给出>< 来表示严格正函数的首选表示。对于容器来说，这很简单。
（S <| P）>< （S'<| P'）=（S * S'）<| \ {（s，s'） - > P s * P's'}
结论
容器在其标准化的Sigma-then-Pi形式中，并不打算成为数据的有效机器表示。但是，一个给定的函子实现的知识，然而，作为一个容器的演示文稿有助于我们理解其结构并为其提供有用的设备。许多有用的结构可以抽象地用于容器，一次是所有的，当它们必须由其他表示进行个案处理时。所以，是的，学习容器是一个好主意，只要掌握实际实现的更具体结构的基本原理即可。
(As an excuse: the title mimics the title of Why do we need monads?)
There are containers (and indexed ones) (and hasochistic ones) and descriptions. But containers are problematic and to my very small experience it's harder to think in terms of containers than in terms of descriptions. The type of non-indexed containers is isomorphic to Σ — that's quite too unspecific. The shapes-and-positions description helps, but in
⟦_⟧ᶜ : ∀ {α β γ} -> Container α β -> Set γ -> Set (α ⊔ β ⊔ γ)
⟦ Sh ◃ Pos ⟧ᶜ A = ∃ λ sh -> Pos sh -> A
Kᶜ : ∀ {α β} -> Set α -> Container α β
Kᶜ A = A ◃ const (Lift ⊥)
we are essentially using Σ rather than shapes and positions.
The type of strictly-positive free monads over containers has a rather straightforward definition, but the type of Freer monads looks simpler to me (and in a sense Freer monads are even better than usual Free monads as described in the paper).
So what can we do with containers in a nicer way than with descriptions or something else?
To my mind, the value of containers (as in container theory) is their uniformity. That uniformity gives considerable scope to use container representations as the basis for executable specifications, and perhaps even machine-assisted program derivation.
Containers: a theoretical tool, not a good run-time data representation strategy
I would not recommend fixpoints of (normalized) containers as a good general purpose way to implement recursive data structures. That is, it is helpful to know that a given functor has (up to iso) a presentation as a container, because it tells you that generic container functionality (which is easily implemented, once for all, thanks to the uniformity) can be instantiated to your particular functor, and what behaviour you should expect. But that's not to say that a container implementation will be efficient in any practical way. Indeed, I generally prefer first-order encodings (tags and tuples, rather than functions) of first-order data.
To fix terminology, let us say that the type Cont of containers (on Set, but other categories are available) is given by a constructor <| packing two fields, shapes and positions
S : Set
P : S -> Set
(This is the same signature of data which is used to determine a Sigma type, or a Pi type, or a W type, but that does not mean that containers are the same as any of these things, or that these things are the same as each other.)
The interpretation of such a thing as a functor is given by
[_]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
And we're already winning. That's map implemented once for all. What's more, the functor laws hold by computation alone. There is no need for recursion on the structure of types to construct the operation, or to prove the laws.
Descriptions are denormalized containers
Nobody is attempting to claim that, operationally, Nat <| Fin gives an efficient implementation of lists, just that by making that identification we learn something useful about the structure of lists.
Let me say something about descriptions. For the benefit of lazy readers, let me reconstruct them.
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 }
Values in Desc describe functors whose fixpoints give datatypes. Which functors do they describe?
[_]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')
We inevitably have to work by recursion over descriptions, so it's harder work. The functor laws, too, do not come for free. We get a better representation of the data, operationally, because we don't need to resort to functional encodings when concrete tuples will do. But we have to work harder to write programs.
Note that every container has a description:
sg S \ s -> pi (P s) \ _ -> var
But it's also true that every description has a presentation as an isomorphic container.
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
That's to say, containers are a normal form for descriptions. It's an exercise to show that [ D ]D X is naturally isomorphic to [ ContD D ]C X. That makes life easier, because to say what to do for descriptions, it's enough in principle to say what to do for their normal forms, containers. The above mapD operation could, in principle, be obtained by fusing the isomorphisms to the uniform definition of mapC.
Differential structure: containers show the way
Similarly, if we have a notion of equality, we can say what one-hole contexts are for containers uniformly
_-[_] : (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 ] })
That is, the shape of a one-hole context in a container is the pair of the shape of the original container and the position of the hole; the positions are the original positions apart from that of the hole. That's the proof-relevant version of "multiply by the index, decrement the index" when differentiating power series.
This uniform treatment gives us the specification from which we can derive the centuries-old program to compute the derivative of a polynomial.
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')
How can I check that my derivative operator for descriptions is correct? By checking it against the derivative of containers!
Don't fall into the trap of thinking that just because a presentation of some idea is not operationally helpful that it cannot be conceptually helpful.
On "Freer" monads
One last thing. The Freer trick amounts to rearranging an arbitrary functor in a particular way (switching to Haskell)
data Obfuncscate f x where
(:<) :: forall p. f p -> (p -> x) -> Obfuncscate f x
but this is not an alternative to containers. This is a slight currying of a container presentation. If we had strong existentials and dependent types, we could write
data Obfuncscate f x where
(:<) :: pi (s :: exists p. f p) -> (fst s -> x) -> Obfuncscate f x
so that (exists p. f p) represents shapes (where you can choose your representation of positions, then mark each place with its position), and fst picks out the existential witness from a shape (the position representation you chose). It has the merit of being obviously strictly positive exactly because it's a container presentation.
In Haskell, of course, you have to curry out the existential, which fortunately leaves a dependency only on the type projection. It's the weakness of the existential which justifies the equivalence of Obfuncscate f and f. If you try the same trick in a dependent type theory with strong existentials, the encoding loses its uniqueness because you can project and tell apart different choices of representation for positions. That is, I can represent Just 3 by
Just () :< const 3
or by
Just True :< \ b -> if b then 3 else 5
and in Coq, say, these are provably distinct.
Challenge: characterizing polymorphic functions
Every polymorphic function between container types is given in a particular way. There's that uniformity working to clarify our understanding again.
If you have some
f : {X : Set} -> [ S <| T ]C X -> [ S' <| T' ]C X
it is (extensionally) given by the following data, which make no mention of elements whatsoever:
toS : S -> S'
fromP : (s : S) -> P' (toS s) -> P s
f (s , k) = (toS s , k o fromP s)
That is, the only way to define a polymorphic function between containers is to say how to translate input shapes to output shapes, then say how to fill output positions from input positions.
For your preferred representation of strictly positive functors, give a similarly tight characterisation of the polymorphic functions which eliminates abstraction over the element type. (For descriptions, I would use exactly their reducability to containers.)
Challenge: capturing "transposability"
Given two functors, f and g, it is easy to say what their composition f o g is: (f o g) x wraps up things in f (g x), giving us "f-structures of g-structures". But can you readily impose the extra condition that all of the g structures stored in the f structure have the same shape?
Let's say that f >< g captures the transposable fragment of f o g, where all the g shapes are the same, so that we can just as well turn the thing into a g-structure of f-structures. E.g., while [] o [] gives ragged lists of lists, [] >< [] gives rectangular matrices; [] >< Maybe gives lists which are either all Nothing or all Just.
Give >< for your preferred representation of strictly positive functors. For containers, it's this easy.
(S <| P) >< (S' <| P') = (S * S') <| \ { (s , s') -> P s * P' s' }
Conclusion
Containers, in their normalized Sigma-then-Pi form, are not intended to be an efficient machine representation of data. But the knowledge that a given functor, implemented however, has a presentation as a container helps us understand its structure and give it useful equipment. Many useful constructions can be given abstractly for containers, once for all, when they must be given case-by-case for other presentations. So, yes, it is a good idea to learn about containers, if only to grasp the rationale behind the more specific constructions you actually implement.
这篇关于为什么我们需要容器？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
