haskell - 我们在 Coyoneda 上申请的 "natural transformations"是为了得到一个 Functor 实际上是 "natural transformations"吗？

Question

我有一个关于使用的类型的性质的理论问题
很多解释 Coyoneda 引理的例子。它们通常被称为
作为“自然变换”，据我所知，仿函数之间的映射。
令我困惑的是，在这些示例中，它们有时映射自 Set。到某个仿函数 F .因此，它实际上并不是仿函数之间的映射，而是更轻松一些。

这是有问题的代码:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
module Coyo where

import           Data.Set (Set)
import qualified Data.Set as Set

data Coyoneda f a where
  Coyoneda :: (b -> a) -> f b -> Coyoneda f a

instance Functor (Coyoneda f) where
  fmap f (Coyoneda c fa) =  Coyoneda (f . c) fa

set :: Set Int
set = Set.fromList [1,2,3,4]

lift :: f a -> Coyoneda f a
lift fa = Coyoneda id fa

lower :: Functor f => Coyoneda f a -> f a
lower (Coyoneda f fa) = fmap f fa

type NatT f g = forall a. f a -> g a

coyoset :: Coyoneda Set Int
coyoset = fmap (+1) (lift set)

applyNatT :: NatT f g -> Coyoneda f a -> Coyoneda g a
applyNatT n (Coyoneda f fa) = Coyoneda f (n fa)

-- Set.toList is used as a "natural transformation" here
-- while it conforms to the type signature of NatT, it
-- is not a mapping between functors `f` and `g` since
-- `Set` is not a functor.
run :: [Int]
run = lower (applyNatT Set.toList coyoset)

我在这里有什么误解？

编辑:在 freenode 中讨论了#haskell 之后，我想我需要稍微澄清一下我的问题。它基本上是:“什么是 Set.toList范畴理论意义？因为它显然(？)不是自然的转变”。

Answer 1

对于 n要成为 Haskell 中的自然转换，它需要服从(对于所有 f)

(fmap f) . n == n . (fmap f)

Set.toList 的情况并非如此。 .

fmap (const 0) . Set.toList        $ Set.fromList [1, 2, 3] = [0, 0, 0]
Set.toList     . Set.map (const 0) $ Set.fromList [1, 2, 3] = [0]

相反，它遵循一套不同的法律。还有一个转换 n'以另一种方式返回，使得以下内容成立

n' . (fmap f) . n == fmap f

如果我们选择 f = id并应用仿函数定律 fmap id == id我们可以看到这意味着 n' . n == id因此我们有一个类似的公式:

(fmap f) . n' . n == n' . (fmap f) . n == n' . n . (fmap f)

n = Set.toList和 n' = Set.fromList遵守这条法律。

Set.map (const 0) . Set.fromList   . Set.toList        $ Set.fromList [1, 2, 3] = fromList [0]
Set.fromList      . fmap (const 0) . Set.toList        $ Set.fromList [1, 2, 3] = fromList [0]
Set.fromList      . Set.toList     . Set.map (const 0) $ Set.fromList [1, 2, 3] = fromList [0]

除了观察到 Set 之外，我不知道我们可以称之为什么。是列表的等价类。 Set.toList找到等价类的代表成员和 Set.fromList是商。

可能值得注意的是 Set.fromList是一种自然的转变。至少它在 的合理子类别中。哈斯克在哪里 a == b暗示 f a == f b (这里 == 是来自 Eq 的平等)。这也是 的子类别哈斯克在哪里 Set是仿函数；它不包括 degenerate things like this .

leftaroundabout还指出 Set.toList是 子类别的自然变换哈斯克其中态射限于 injective functions where f a == f b implies a == b .