Le "trasformazioni naturali" che applichiamo a Coyoneda sono effettivamente "trasformazioni naturali" per un Functor?

Question

Ho una domanda teorica sulla natura di un tipo che viene utilizzato in un sacco di esempi che spiegano il lemma di Coyoneda. Solitamente si riferiscono a come "trasformazioni naturali" che a mia conoscenza mappano tra i funtori. Ciò che mi indovina è che in questi esempi a volte vengono mappati da Set a qualche functor F. Quindi non è davvero una mappatura tra i funtori ma qualcosa di un po 'più rilassato.

Ecco il codice in questione:

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

Cosa sto equivoco?

MODIFICA: Dopo una discussione su #haskell in freenode, penso di aver bisogno di chiarire un po 'la mia domanda. È fondamentalmente: "Che cos'è Set.toList in un senso teorico di categoria ? Poiché è ovviamente (?) Non una trasformazione naturale".

Answer 1

Per n per essere un transfomation naturale in Haskell deve obbedire (per tutti f)

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

Questo non è il caso per 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] 

Invece obbedisce a un diverso insieme di leggi. C'è un'altra trasformazione n' indietro l'altro modo tale che vale quanto segue

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

Se scegliamo f = id e applichiamo la legge funtore fmap id == id possiamo vedere che questo implica che n' . n == id e quindi abbiamo una formula simile:

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

n = Set.toList e n' = Set.fromList obbediscono a questa legge.

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] 

Non so quello che possiamo chiamare questo diverso osservando che Set è una classe di equivalenza delle liste. Set.toList trova un membro rappresentativo della classe di equivalenza e Set.fromList è il quoziente.

Vale la pena notare che Set.fromList è una trasformazione naturale. Almeno è nella ragionevole sottocategoria di Hask dove a == b implica f a == f b (qui == equivale a Eq). Questa è anche la sottocategoria di Hask dove Set è un functor; esclude degenerate things like this.

leftaroundabout inoltre sottolineato che Set.toList è una trasformazione naturale dalla sottocategoria di Hask dove morfismi sono limitati a injective functions where f a == f b implies a == b.