如果`zip`是一个合法类型类的方法，那么它属于哪个类型类？

Question

如果`zip`是一个合法类型类的方法，那么它属于哪个类型类？

4

为什么会有这个问题 一个人可能会说zip是一种Applicative方法，通常的实例是ZipList。我不喜欢它，因为它不安全。我也不喜欢Align，因为它过于复杂，并且对于通常的情况来说不够具体。

合法类 在Haskell中，一些类型类可以被称为“合法”。这意味着它们带有必须满足的等式-该类的法律。这些法律通常来自于编程某个方面的范畴理论概念化。例如，Monad是通过同名的范畴理论设备对计算 (无论其含义如何)进行概念化。

叠加事物 与事物盒子想要做的通常操作是将它们放在彼此上方，如果它们是幺半群，则它们将融合。

例如：

不够法律 通过幺半群函子和相应的Applicative类型类来概念化这个概念。然而，令人讨厌的是，通常有两种定义Applicative的方式都看起来合适。为什么呢？我认为答案是"法律不够"。

例如：

对于算术运算：
- Sum 单子群是实际的“自身单子群”。它仅适用于相同类型的事物。例如，您不能将质量和力相加。
- Product 单子群将具有维度 a 和 b 的数字转换为具有维度 c 的数字。相乘质量和力是合法的，并将我们带到温暖。
因此，正确的单子群选择可以从类型中推断出来。
对于列表：
- 通常的列表直和是更安全的一种。它可以轻松处理任意数量的元素，以及通过像LogicT这样的“对角线过程”定义来处理共限制数量的元素。
- ZipList 定义明显不安全。它被定义为：给定两个长度不同的列表，将较长的一个裁剪到与较短的长度相同。
- 长度索引向量是允许通过要求给定的列表具有相同长度来安全定义 zip 的设备。
对于矩阵：
- 通常的矩阵加法具有尺寸同质性的（非常合理的）要求，与上面提到的长度索引向量相同。由于矩阵通常用于各种现实世界的模拟，例如 3D 图形，一旦矩阵开始被裁剪或填充为零，人们会立即抱怨，因此类似于上面的 ZipList 的 ZipMatrix 定义并不吸引人。
- 更奇怪的Kronecker 乘积类似于列表的直积。它还允许定义Monad。

两种情况 从这些示例中可以看出，在我们称之为“单子群”或“单子范畴函子”的事物中混杂着两个不同的想法，这种区别对于编程非常重要（与纯理论不同），因为它可以清除混乱，消除不安全因素，并且主要是因为在每种情况下都有两个完全不相关的算法需要运行。

我认为单源函子的可逆性（也称为“强度”）可能很重要。但是对于Peano自然数的Sum和Product单源操作的结果是无法区分的。（我不确定它们是否可以被认为是单源自函子。）所以，我猜测类型的变化是关键。甚至物理数量的乘法也不能作为Monoid进行类型检查！

附注：存在一种基于笛卡尔积的长度索引向量和基于Kronecker乘法的矩阵的Monad实例，其中使用某种形式的fold zip作为join。

- Ignat Insarov

什么是可逆的？显而易见的定义是“如果liftA2(,)xs ys==liftA2(,)xs'ys'，那么xs==xs'和ys==ys'”。但是通常用于列表的Applicative实例（我认为您称之为“直和”）被认为是可逆的，但不符合此定义（例如liftA2(,)[] [()] == liftA2(,)[()] []），因此我不清楚您在这里想要什么。（这不是关于空值的争论：还有一些非空列表会破坏可逆性。） - Daniel Wagner

2

考虑向量和矩阵，可能有一些二元操作你没有考虑过。除了笛卡尔积类型((a -> b -> c) -> v n a -> v m b -> v (n * m) c)和zip类型((a -> b -> c) -> v n a -> v n b -> v n c)之外，还有一种用于矩阵的收缩类型：Monoid c => (a -> b -> c) -> m x y a -> m y z b -> m x z c`。话虽如此，我认为这个操作最适合放在一个形状索引应用程序中。这适用于向量，因为它们显然是可压缩的，并且大小很容易表达。它也适用于函数，但不适用于映射。 - Dan Robertson

对于矩阵加法来说，使用零填充实际上是相当明智的选择：动态大小的矩阵表示有限秩线性映射 ℝ^∞ → ℝ^∞，如果一个矩阵比另一个矩阵短，那么它的其它条目就被视为零。大多数数据语言（如Matlab传统）之所以在添加不同维度的矩阵时抛出错误，是因为它们没有正确的类型系统。在像Haskell这样的良好类型化语言中，“矩阵”的正确表示方式是作为线性映射范畴的一部分。 - leftaroundabout

重新阅读问题，我认为它并没有明确地聚焦。你首先谈到了applicatives，但接下来的要点却是关于monoids的。请记住，“monoidal functor”与Monoid实际上没有太多关系：前者指的是单一的_类型级别的monoid_((),(,))，后者指的是Haskell类型中各种值级别的monoid。 - leftaroundabout

@leftaroundabout 我不确定我是否准备好同意。 (1) “这就是它的工作原理”也可以用于隐式状态和指针算术。 (2) 我认为元组是自由幺半群的一个实例，就像列表或hlist一样。具体来说，人们通常将事物 x :: A 和 y :: B 放在元组 (x，y) 中，因为稍后将可用函数 f :: A-> B-> C 将它们融合在一起。因此，人们可以将它们包装在 data W = WA A | WB B | WC C 中，并定义一个 instance Monoid W where mappend (WA x) (WB y) = WC $ f x y。这能更好地证明我的论点吗？ - Ignat Insarov

显示剩余10条评论

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- duplode · Accepted Answer

精确的压缩（如safe包所称）可以通过Representable类来表达。有相当数量的理论与Representable相关。对于我们当前的目的，我们可以关注于...

如果Functor f具有到(->) x的同构，则f是Representable。

并且:

在Haskell类型范畴中，可表示的自函子同构于reader monad，因此可以免费继承大量属性。

Representable函子等同于某个类型的函数（例如，一个同构于Bool -> a的同态对，以及一个同构于Nat -> a的无限流），因此可以通过逐点组合函数来实现精确压缩。这就是mzipRep的作用，它是MonadZip的mzip的默认实现：

mzipRep :: Representable f => f a -> f b -> f (a, b)
mzipRep as bs = tabulate (index as &&& index bs)

MonadZip 是一个相当笨拙的类（主要是实现了 MonadComprehensions 扩展的一部分），但它有一个相关的法则，我将在非单子术语中重新陈述它：

信息保存：如果 () <$ u = () <$ v，那么 munzip (mzip u v) = (u, v)

换句话说，如果 u 和 v 具有相同的形状，则 mzip 不会丢失信息（因此可以通过 munzip 撤消）。由于 Representable 意味着只有一种可能的形状，它允许我们放弃这个条件，从而得到精确的压缩。

侧记：

ZipList 的定义显然是不安全的。它被定义为，给定两个不同长度的列表，将较长的列表裁剪为较短的长度。

我想这取决于你想用 zipping 做什么。有时你需要精确的 zipping，有时则不需要（例如，考虑使用 zip [0..] 将索引附加到列表的常见技巧）；有时填充而不是修剪才是有意义的（参见 leftaroundabout's comment）。这就是为什么我更喜欢称精确的 zipping 为“精确”，而不是“安全”。

然而，有一个令人烦恼的复杂性，那就是通常有两种方式来定义适用于 Applicative 的方法，它们都看起来适合。为什么会这样？我认为答案是“定律不足”。

我非常不同意这个观点：如果一个类允许某种数据类型有多个实例，那么它就是未经说明的。我更愿意说，例如，使用笛卡尔积应用程序的列表和使用压缩应用程序的列表是不同的结构，由相关的态射所特征化 - 只是碰巧它们可以通过相同的数据类型在Haskell中表示。