“ arr fst”如何自然转变？

问题描述

我刚才问this question。关于以下箭头法则：

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

在Asad Saeeduddin帖子下的评论中，以自然转化的方式对其进行了解释。我想检查一下我对他们的解释是否正确，并将其与Bartosz Milewski's article on natural transformations进行比较。

因此，自然变换的定义是：

我们有两个类别C和D和函子F,G : C ~> D。自然变换α是D中的箭头族，

1. 这些箭头从F的结果到G的结果。也就是说，a中的每个对象C都有一个箭头（在α 处称为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。 不要可以更轻松地根据类型进行思考，因为Category和Arrow类可以帮助我们构造类别的箭头，而不是对象

这是对的吗

此外，Bartosz Milewski wrote those ideas down像这样：

fmap f . alpha = alpha . fmap f

据我所知，出于我们的目的，我们需要一种更通用的形式，因为此处alpha :: forall a. F a -> G a仅针对与 Hask 相关的类别。还是我错了？ fmap在这张图片中位于哪个地方？

解决方法

据我所知：

• 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 的每一个选择都为我们提供了 (,c) 内函子和 k 范畴中的恒等函子之间的自然转换。执行专业化为我们提供了一个看起来更像是自然转换的签名：

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

此外，Bartosz Milewski wrote those ideas down 像这样：

fmap f . alpha = alpha . fmap f

据我所知，为了我们的目的，我们需要一个更通用的形式 此处 alpha :: forall a. F a -> G a 仅将 Hask 作为 它适用的类别。还是我错了？ fmap 在哪个地方 这张照片？

也正确。 fmap 必须被所涉及的函子的任何适当的态射映射替换。在您的示例中，这些恰好是 first 和 id，正如您之前所注意到的，这使我们回到了我们开始的箭头定律。

（至于替换 fmap，Functor 的方法从特定函子态射映射中抽象出来，通过更一般的类比，需要进行适当的安排，以便我们可以表达涉及非Haskell 代码中的 Hask 类别。您可能想看看 constrained-categories 和 data-category 如何处理。）

,

您无需担心额外的类别，因为arr fst并不涉及任意的Arrow，仅涉及其(,)实例。

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