‘`arr’是一种自然的转变吗？

Question

不久前我问过这个问题。它是关于以下箭头定律的：

arr fst . first f = f . arr fst -- (.) :: Category k => k b c -> k a b -> k a c

在文章下面的注释中，Saeeduddin用自然转换解释了它。我想检查一下他们的解释是否正确，并将其与Bartosz Milewski关于自然变换的文章进行比较。

因此，自然转换的定义如下：

我们有两类C和D以及函子F, G : C ~> D。自然转换α是D中的一系列箭头，因此：

1. 这些箭头从F的结果到G的结果。也就是说，对于C中的每个对象，都有一个箭头(称为 a) at a) α_a :: F a ~> G a的组件)。
2. 对于每一个f :: a ~> b，a和b都是C中的对象，持有：Gf . α_a = α_b . Ff。这就是自然性。

基本上，我们需要计算出我们的例子中的四个变量：C、D、F和G。

据我所知：

• C和D是相同的任意类型，其中k a b是箭头，其中k是我们使用的Arrow实例。因此，F和G是内毒素。
• F是(, c)，G是Identity。换句话说，如果我们不再使用类型，我们将F映射为first，G映射为id。如果和Arrow类帮助我们构造类别的箭头，而不是对象，那么从类型的角度来考虑可能更容易一些，而不是Arrow。

是这样的吗？

此外，巴托斯·米列夫斯基把这些想法写下来了喜欢这样：

fmap f . alpha = alpha . fmap f

据我所知，为了我们的目的，我们需要一个更通用的形式，因为在这里，alpha :: forall a. F a -> G a只将Hask作为它所使用的类别来处理。还是我错了？fmap在这张照片上有什么地方？

Answer 1

据我所知：

• C和D是相同的任意类型，其中k a b是箭头，其中k是我们使用的Arrow实例。因此，F和G是内毒素。
• F是(, c)，G是Identity。换句话说，如果我们不再使用类型，我们将F映射为first，G映射为id。..。

是的，就是这样。k和c在arr fst :: k (b, c) b中的每一种选择都给了我们在k-category中的(, c)内切函数和身份函子之间的自然转换。进行专业化给了我们一个更明显的特征，它看起来更像是一种自然转变的特征：

arr @K (fst @_ @C) :: forall b. K (b, C) b

此外，巴托斯·米列夫斯基把这些想法写下来了喜欢这样： fmap f.阿尔法=阿尔法fmap f 据我所知，为了我们的目的，我们需要一个更通用的形式，因为在这里，alpha :: forall a. F a -> G a只将Hask作为它所使用的类别来处理。还是我错了？fmap在这张照片上有什么地方？

同样正确。对于涉及到的函子，fmap必须被适当的态射映射所取代。在您的例子中，这些恰好是first和id，正如您之前注意到的，这使我们回到了我们开始使用的箭头定律。

(至于替代fmap，从特定函子态射映射中抽象出的Functor方法，用一个更一般的类似物来表示，这需要作出适当的安排，以便我们可以在Haskell代码中表示涉及非Hask范畴的函子。您可能想看看http://hackage.haskell.org/package/constrained-categories-0.4.1.0/docs/Control-Functor-Constrained.html和https://hackage.haskell.org/package/data-category-0.10/docs/Data-Category-Functor.html如何处理这个问题。)

Answer 2

您不需要担心额外的类别，因为arr fst不涉及任意的Arrow，而是它的(,)实例。

在Haskell中，f a -> g a型函数对于某些函子f和c是一种自然变换。在arr fst :: (b -> c) -> (b, c)的例子中，让f ~ (->) b和g ~ (,) b。