为什么我们需要容器？

(作为借口:标题模仿了为什么我们需要monad？)

有容器(和索引的)(和无用的)和描述.但是容器是有问题的,根据我很小的经验,就容器而言,比描述更难以思考.非索引容器的类型是同构的?- 这是非常不明确的.形状和位置描述有帮助,但在

?_?? : ? {? ? ?} -> Container ? ? -> Set ? -> Set (? ? ? ? ?)
? Sh ? Pos ?? A = ? ? sh -> Pos sh -> A

K? : ? {? ?} -> Set ? -> Container ? ?
K? A = A ? const (Lift ?)

我们本质上是使用?而不是形状和位置.

容器上的严格正面免费monad的类型有一个相当简单的定义,但Freermonad 的类型对我来说看起来更简单(在某种意义上,Freermonad甚至比文章中Free描述的通常monad 更好).

那么我们可以用更好的方式来做容器而不是描述或其他什么呢？

1> pigworker..：

---

在我看来,容器的价值(如容器理论中)是它们的一致性.这种一致性为使用容器表示作为可执行规范的基础提供了相当大的余地,甚至可能是机器辅助程序的推导.

容器:理论工具,而不是良好的运行时数据表示策略

我不建议将(规范化的)容器的固定点作为实现递归数据结构的一种通用方法.也就是说,知道给定的函子具有(最多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

但这不是容器的替代品.这是容器展示的轻微描述.如果我们有强大的存在和依赖类型,我们可以写

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 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)

也就是说,在容器之间定义多态函数的唯一方法是说如何将输入形状转换为输出形状,然后说明如何从输入位置填充输出位置.

对于您首选的严格正函子的表示,对多态函数进行类似的严格表征,从而消除对元素类型的抽象.(为了描述,我会将它们的可还原性完全用于容器.)

挑战:捕捉"转座"

给定两个函子,f并且g很容易说出它们的组成f o g是什么:(f o g) x包装内容f (g x),给我们" f-structures of g-structures".但是你能否轻易地施加额外的条件,即g存储在f结构中的所有结构都具有相同的形状？

假设f >< g捕获所有形状相同的转置片段,这样我们就可以将事物转化为-structure of -structures.例如,虽然给出了不规则的列表列表,但给出了矩形矩阵; 给出全部或全部的列表.f o gggf[] o [][] >< [][] >< MaybeNothingJust

给出><您严格积极的仿函数的首选表示.对于容器来说,这很容易.

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

结论

容器采用标准化的Sigma-then-Pi形式,并非旨在成为数据的有效机器表示.但是,然而,实现的给定仿函数具有作为容器的表示的知识有助于我们理解其结构并为其提供有用的设备.对于容器,可以抽象地给出许多有用的结构,一旦适用于所有情况,必须根据具体情况给出其他演示.所以,是的,了解容器是个好主意,如果只是为了掌握实际实现的更具体结构背后的基本原理.