我们在Coyoneda上应用"自然变换"来实现Functor实际上的"自然变换"吗？

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是一种自然的转变.至少它在Hask的合理子类别中a == b暗示f a == f b(这里==是相等Eq).这也是Hask的子类别,其中Set是一个仿函数; 它排除了这样的堕落之物.

leftaroundabout还指出,这Set.toList是Hask子类别的自然变换,其中态射被限制在f a == f b暗示的内射函数a == b.