Come posso mostrare che la traversata interagisce sensibilmente con fmap?

Question

Sembra intuitivamente evidente che la seguente legge dovrebbe contenere:

traverse f . fmap g = traverse (f . g) 

L'unica Traversable legge che sembra da applicare direttamente è

fmap g = runIdentity . traverse (Identity . g) 

che cambia il problema di

traverse f . runIdentity . traverse (Identity . g) 

L'unica legge che sembra avere vagamente la forma giusta da applicare a questo è e legge sulla naturalità. Ciò, tuttavia, riguarda le trasformazioni applicative e non vedo nessuna di quelle intorno.

A meno che non manchi qualcosa, l'unica cosa rimasta è una prova di parametrismo, e non ho ancora avuto la minima idea di come scriverli.

Answer 1

Si noti che questa dimostrazione non è effettivamente necessaria, in quanto il risultato in questione è davvero un teorema gratuito. Vedi la risposta di Reid Barton.

Credo che questo farà:

traverse f . fmap g -- LHS 

Per la legge fmap/traverse,

traverse f . runIdentity . traverse (Identity . g) 

Dal fmap per Identity è efficace id,

runIdentity . fmap (traverse f) . traverse (Identity . g) 

IlLa leggeoffre un modo per comprimere due traversamenti in uno, ma dobbiamo prima introdurre Compose utilizzando getCompose . Compose = id.

runIdentity . getCompose . Compose . fmap (traverse f) . traverse (Identity . g) 
-- Composition law: 
runIdentity . getCompose . traverse (Compose . fmap f . Identity . g) 

nuovamente usando l'Identityfmap,

runIdentity . getCompose . traverse (Compose . Identity . f . g) 

Compose . Identity è una trasformazione applicativa, così da naturalezza,

runIdentity . getCompose . Compose . Identity . traverse (f . g) 

inversi collasso,

traverse (f . g) -- RHS 

leggi e corollari invocato per ragioni di completezza:

-- Composition: 
traverse (Compose . fmap g . f) = Compose . fmap (traverse g) . traverse f 
-- Naturality: 
t . traverse f = traverse (t . f) -- for every applicative transformation t 
-- `fmap` as traversal: 
fmap g = runIdentity . traverse (Identity . g) 

Quest'ultima infatti risulta dalla legge di identità, traverse Identity = Identity, più l'unicità di fmap.

Answer 2

Secondo lambdabot è un teorema gratuito (parametrricità).

In risposta a @free traverse :: (a -> F b) -> T a -> F (T b), lamdabot produce

$map_F g . h = k . f => $map_F ($map_T g) . traverse h = traverse k . $map_T f 

impost g = id in modo che h = k . f.Quindi la conclusione diventa

traverse (k . f) = traverse k . fmap f