Sind die "natürlichen Transformationen", die wir auf Coyoneda anwenden, um einen Functor tatsächlich "natürliche Transformationen" zu bekommen?

Question

Ich habe eine theoretische Frage über die Art eines Typs, der in viele Beispiele verwendet wird, die das Coyoneda-Lemma erklären. Sie werden normalerweise als "natürliche Transformationen" bezeichnet, die meines Wissens Abbildungen zwischen Funktoren sind. Was mich verwirrt ist, dass sie in diesen Beispielen manchmal von Set zu einem Funktor F mappen. Es ist also nicht wirklich eine Zuordnung zwischen Funktoren, sondern etwas entspannteres. Hier

ist der Code in Frage:

{-# 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) 

Was ich hier Missverständnis?

EDIT: Nach einer Diskussion über #haskell in freenode Ich denke, ich muss meine Frage ein wenig klären. Es ist im Grunde: "Was ist Set.toList in einem kategorientheoretischen Sinn? Da ist es offensichtlich (?) Keine natürliche Transformation".

Answer 1

Für n eine natürliche transfomation in Haskell, um es (für alle f)

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

Dies ist nicht der Fall für Set.toList gehorchen muss.

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] 

Stattdessen gehorcht es einem anderen Satz von Gesetzen. Es gibt eine andere Transformation n' wieder in die andere Richtung, so dass die folgende

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

hält Wenn wir f = id wählen und anwenden, die Funktors Gesetz fmap id == id können wir sehen, dass dies bedeutet, dass n' . n == id und damit wir eine ähnliche Formel:

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

n = Set.toList und n' = Set.fromList gehorchen diesem Gesetz.

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] 

Ich weiß nicht, was wir diese andere als die Beobachtung nennen können, dass Set eine Äquivalenzklasse von Listen ist. Set.toList findet ein repräsentatives Mitglied der Äquivalenzklasse und Set.fromList ist der Quotient.

Es ist wahrscheinlich erwähnenswert, dass Set.fromList eine natürliche Transformation ist. Zumindest ist es auf der vernünftigen Unterkategorie Hask wo a == b impliziert f a == f b (hier == ist die Gleichheit von Eq). Dies ist auch die Unterkategorie Hask wo Set ein Funktor ist; es schließt degenerate things like this aus.

leftaroundabout wies auch darauf hin, dass Set.toList auf der Unterkategorie des Hask eine natürliche Transformation ist wo morphisms zu injective functions where f a == f b implies a == b beschränkt ist.