训练员和箭之间有什么关系？ [英] What's the relationship between profunctors and arrows?

问题描述

显然，每个箭头都是 强大的 工具。事实上， ^>> 和>> ^ 对应于 lmap 和 rmap 。并且 first'和 second'与第一和第二。同样，每个 ArrowChoice 也是 选择 。 b
$ b

组成他们的能力。如果我们添加构图，我们会得到一个箭头？换句话说，如果一个（强）分解器也是类别，它已经是一个箭头了吗？如果没有，缺少的是什么？

解决方案

。如果我们添加作文，我们会得到一个箭头吗？

MONOIDS

这正是计算为猿猴的概念的第6部分所解决的问题，它将解包来自（相当密集的）箭头的分类语义。 概念是一篇很好的论文，因为尽管深入到类别理论中，它（1）并不假设读者对抽象代数的概念不仅仅是粗略的知识，并且（2）用Haskell代码说明了大多数偏头痛诱导数学。我们可以在这里简要总结这篇论文的第6部分：

假设我们有

  class Profunctor p where 
 dimap ::（contra' - > contra） - > （co  - > co'） - > p contra co  - > p contra'co'
  

你的浸润标准，负分正确的dividin编码哈斯克尔。现在这个数据类型，

  data（⊗）f g contra co = forall x。 （f contra x）⊗（gx co）
  

在 Data.Profunctor.Composition ，就像构建函数一样。例如，我们可以演示一个合法的实例 Profunctor ：

  instance （Profunctor f，Profunctor g）=> Profunctor（f⊗g）其中
 dimap contra co（f⊗g）=（dimap contra id f）d（dimap id co g）
  

我们会手动证明它是合法的，因为时间和空间的原因。

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

  class Profunctor p => ProfunctorMonoid p其中
 e ::（a  - > b） - > p a b 
 m ::（p⊗p）a b  - > pab 
  

这就是更多手势的编码方式在Haskell。具体来说，这是monoid类别 Pro 中的monoid，它是仿函数类别 [C ^ op x C，Set] code>，其中⊗作为张量， Hom 作为其单位。所以这里有很多超类型的数学词典来解压缩，但是你应该只是阅读论文。

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

 实例ProfunctorMonoid p =>类别p其中
 id = dimap id id 
（。）pbc pab = m（pab⊗pbc）
 
实例ProfunctorMonoid p =>箭头p其中
 arr = e 
 first =未定义
 
实例箭头p => Profunctor p其中
 lmap =（^>>）
 rmap =（>> ^）
 
实例Arrow p => ProfunctorMonoid p其中
 e = arr 
 m（pax⊗pxb）= pax>> pxb 
  

当然，我们在此忽略类别类法则，但正如文章所显示的那样，

现在我几乎说因为我们无法实现 first 。我们实际上做的是 ProfunctorMonoid 和前置箭头之间的同构性。本文调用 Arrow 没有第一个 a 前箭头。然后它继续显示：

  class Profunctor p => StrongProfunctor p其中
 first :: p x y  - > p（x，z）（y，z）
 
 class StrongProfunctor p => StrongProfunctorMonoid p其中
 e ::（a  - > b） - > p a b 
 m ::（p⊗p）a b  - > pab 
  

对于所需的同构 Arrow 。 强这个词来源于类别理论中的一个特定概念，并且这篇论文写得比我所能想到的写得更好，文字更丰富。

所以总结一下：

• 类工具类中的monoid是前置箭头，反之亦然。 （这篇论文的前一版本使用术语弱箭头而不是前置箭头，这也可以。）

由于monad是endofunctors类别中的幺半群，所以我们可以考虑SAT类比 Functor：Profunctor :: Monad：Arrow 。这是计算单元论的真正主旨。
• 幺半群和monoidal类别是温和的海洋生物，无处不在，它是一些学生可能会在没有被教授monoids的情况下通过计算机科学或软件工程教育而感到羞耻。




• Haskell很有趣。

Apparently, every Arrow is a Strong profunctor. Indeed ^>> and >>^ correspond to lmap and rmap. And first' and second' are just the same as first and second. Similarly every ArrowChoice is also Choice.

What profunctors lack compared to arrows is the ability to compose them. If we add composition, will we get an arrow? In other words, if a (strong) profunctor is also a category, is it already an arrow? If not, what's missing?

解决方案

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

MONOIDS

This is exactly the question tackled in section 6 of "Notions of Computation as Monoids," which unpacks a result from the (rather dense) "Categorical semantics for arrows". "Notions" is a great paper because while it dives deep into category theory it (1) doesn't assume the reader has more than a cursory knowledge of abstract algebra and (2) illustrates most of the migraine-inducing mathematics with Haskell code. We can briefly summarize section 6 of the paper here:

Say we have

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

Your bog-standard, negative-and-positive dividin' encoding of profunctors in Haskell. Now this data type,

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

as implemented in Data.Profunctor.Composition, acts like composition for profunctor. We can, for example, demonstrate a lawful instance Profunctor:

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

We will hand-wave the proof that it is lawful for reasons of time and space.

OK. Now the fun part. Say we this typeclass:

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

This is, with a lot more hand-waving, a way of encoding the notion of profunctor monoids in Haskell. Specifically this is a monoid in the monoidal category Pro, which is a monoidal structure for the functor category [C^op x C, Set] with ⊗ as the tensor and Hom as its unit. So there's a lot of ultraspecific mathematical diction to unpack here but for that you should just read the paper.

We then see that ProfunctorMonoid is isomorphic to Arrow ... almost.

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

Of course we are ignoring the typeclass laws here but, as the paper shows, they do work out fantastically.

Now I said almost because crucially we were unable to implement first. What we have really done is demonstrated an isomorphism between ProfunctorMonoid and pre-arrows .The paper calls Arrow without first a pre-arrow. It then goes on to show that

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

is necessary and sufficient for the desired isomorphism to Arrow. The word "strong" comes from a specific notion in category theory and is described by the paper in better writing and richer detail than I could ever muster.

So to summarize:

• A monoid in the category of profunctors is a pre-arrow, and vice versa. (A previous version of the paper used the term "weak arrows" instead of pre-arrows, and that's OK too I guess.)

• A monoid in the category of strong profunctors is an arrow, and vice versa.

• Since monad is a monoid in the category of endofunctors we can think of the SAT analogy Functor : Profunctor :: Monad : Arrow. This is the real thrust of the notions-of-computation-as-monoids paper.

• Monoids and monoidal categories are gentle sea creatures that appear everywhere, and it's a shame that some students will go through computer science or software engineering education without being taught monoids.

• Category theory is fun.

• Haskell is fun.

这篇关于训练员和箭之间有什么关系？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！