haskell - profunctors和箭头有什么关系？

Question

显然，每个 Arrow是 Strong 启蒙者。确实 ^>> 和 >>^对应 lmap和 rmap .和first'和 second'与 first 相同和 second .同样每ArrowChoice也是 Choice .

与箭头相比，profunctors缺乏的是组合它们的能力。如果我们添加合成，我们会得到一个箭头吗？换句话说，如果(强)profunctor 也是 category ，它已经是一个箭头了吗？如果没有，缺少什么？

Answer 1

What profunctors lack compared to arrows is the ability to compose them. If we add composition, will we get an arrow?

单面体

这正是“ Notions of Computation as Monoids”的第 6 节中解决的问题，它从(相当密集的)“ Categorical semantics for arrows”中解压缩了结果。 “概念”是一篇很棒的论文，因为虽然它深入探讨了范畴论，但它 (1) 并没有假设读者对抽象代数有粗略的了解，并且 (2) 用 Haskell 代码说明了大多数诱发偏头痛的数学。我们可以在这里简要总结论文的第 6 节:

说我们有

class Profunctor p where
  dimap :: (contra' -> contra) -> (co -> co') -> p contra co -> p contra' co'

您在 Haskell 中对 profunctor 的沼泽标准、正负除法编码。现在这个数据类型，

data (⊗) f g contra co = forall x. (f contra x) ⊗ (g x co)

在 Data.Profunctor.Composition 中实现, 作用类似于 profunctor 的作文。例如，我们可以展示一个合法的实例 Profunctor :

instance (Profunctor f, Profunctor g) => Profunctor (f ⊗ g) where
  dimap contra co (f ⊗ g) = (dimap contra id f) ⊗ (dimap id co g)

由于时间和空间的原因，我们将举手证明它是合法的。

好的。现在有趣的部分。假设我们这个类型类:

class Profunctor p => ProfunctorMonoid p where
  e :: (a -> b) -> p a b
  m :: (p ⊗ p) a b -> p a b

这是一种在 Haskell 中编码 profunctor monoids 概念的方式。具体来说，这是幺半群类别 Pro 中的一个幺半群。 ，它是仿函数类别 [C^op x C, Set] 的幺半群结构与 ⊗作为张量和 Hom作为它的单位。所以这里有很多超具体的数学词汇要解压，但为此你应该阅读这篇论文。

然后我们看到 ProfunctorMonoid与 Arrow 同构... 几乎。

instance ProfunctorMonoid p => Category p where
  id = dimap id id
  (.) pbc pab = m (pab ⊗ pbc)

instance ProfunctorMonoid p => Arrow p where
  arr = e
  first = undefined

instance Arrow p => Profunctor p where
  lmap = (^>>)
  rmap = (>>^)

instance Arrow p => ProfunctorMonoid p where
  e = arr
  m (pax ⊗ pxb) = pax >> pxb

当然，我们在这里忽略了 typeclass 定律，但正如论文所示，它们确实非常有效。

现在我说几乎是因为至关重要的是我们无法实现 first .我们真正所做的是证明 ProfunctorMonoid 之间的同构。和预箭头。论文调用 Arrow没有 first一个预箭头。然后它继续表明

class Profunctor p => StrongProfunctor p where
  first :: p x y -> p (x, z) (y, z)

class StrongProfunctor p => StrongProfunctorMonoid p where
  e :: (a -> b) -> p a b
  m :: (p ⊗ p) a b -> p a b

对于 Arrow 的所需同构是必要且充分的. “强”这个词来自范畴论中的一个特定概念，这篇论文以比我所能想到的更好的文字和更丰富的细节来描述。

所以总结一下:

profunctor 类别中的幺半群是前箭头，反之亦然。 (该论文的先前版本使用术语“弱箭头”而不是预箭头，我猜这也可以。)

强仿函数类别中的幺半群是箭头，反之亦然。

由于 monad 是内仿函数类别中的幺半群，我们可以想到 SAT 类比 Functor : Profunctor :: Monad : Arrow .这是计算概念作为幺半群论文的真正主旨。

Monoids 和 monoidal 类别是无处不在的温和海洋生物，有些学生会在没有学习过 monoids 的情况下接受计算机科学或软件工程教育，这是一种耻辱。

范畴论很有趣。

haskell 很有趣。