haskell - 我们为什么需要容器？

Question

(作为借口:标题模仿Why do we need monads?的标题)

有containers(和indexed)(和hasochistic)和descriptions。但是容器是problematic，以我的很小的经验，就容器而言，比对描述更难思考。未索引容器的类型与Σ同构—太不确定了。形状和位置描述有帮助，但在

⟦_⟧ᶜ : ∀ {α β γ} -> Container α β -> Set γ -> Set (α ⊔ β ⊔ γ)
⟦ Sh ◃ Pos ⟧ᶜ A = ∃ λ sh -> Pos sh -> A

Kᶜ : ∀ {α β} -> Set α -> Container α β
Kᶜ A = A ◃ const (Lift ⊥)

我们本质上是使用Σ而不是形状和位置。

容器上的严格肯定的免费monad类型具有一个非常简单的定义，但是Freer monads的类型对我来说更简单(从某种意义上说Freer monads甚至比paper中描述的常规Free monad更好)。

那么，与描述或其他方式相比，我们能以更好的方式处理容器吗？

Answer 1

在我看来，容器的值(value)(按照容器理论)是它们的统一性。这种统一性为使用容器表示形式作为可执行规范甚至是机器辅助程序派生的基础提供了很大的范围。

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

我不建议将(规范化)容器的固定点作为实现递归数据结构的良好通用方法。也就是说，知道给定的函子具有(最多等值的)容器表示形式是有帮助的，因为它告诉您可以实例化通用容器功能(由于一致性，很容易实现，一次就可以实现)。给您的特定函子，以及您应该期望的行为。但这并不是说容器实现以任何实际方式都是有效的。确实，我通常更喜欢一阶数据的一阶编码(标签和元组，而不是函数)。

为了修复术语，让我们说容器的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”单子(monad)上

最后一件事。 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-结构g-结构”。但是，您是否可以轻易施加额外条件，即存储在g结构中的所有f结构都具有相同的形状？

假设f >< g捕获了f o g的可转置片段，其中所有g形状都相同，因此我们也可以将其转换为g-结构或f -structures结构。例如，虽然[] o []提供的列表参差不齐，但[] >< []提供的是矩形矩阵； [] >< Maybe给出全部为Nothing或全部Just的列表。

给出><作为您首选的严格表示为正的函子。对于容器，这很容易。

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

结论

规范化的Sigma-then-Pi格式的容器并不旨在成为数据的有效机器表示。但是，对于给定的函子，可以实现，并且可以将其作为容器进行展示，这有助于我们理解其结构并提供有用的设备。当必须针对其他演示文稿逐案给出容器时，可以为容器抽象地给出许多有用的结构。因此，是的，了解容器是一个好主意，只要掌握您实际实现的更具体的构造背后的原理即可。