Quali sono le leggi del functor applicativo in termini di puro e liftA2?

Question

Sto giocando con la formulazione di Applicative in termini di pure e liftA2 (in modo che (<*>) = liftA2 id diventi un combinatore derivato).

Posso pensare a un gruppo di leggi candidate, ma non sono sicuro di quale sarebbe il set minimo.

1. f <$> pure x = pure (f x)
2. f <$> liftA2 g x y = liftA2 ((f .) . g) x y
3. liftA2 f (pure x) y = f x <$> y
4. liftA2 f x (pure y) = liftA2 (flip f) (pure y) x
5. liftA2 f (g <$> x) (h <$> y) = liftA2 (\x y -> f (g x) (h y)) x y
6. ...

Answer 1

Sulla base di McBride e Paterson di laws for Monoidal (sezione 7) Mi piacerebbe SUG Gestire le seguenti leggi per liftA2 e pure.

sinistra e l'identità destra

liftA2 (\_ y -> y) (pure x) fy  = fy 
liftA2 (\x _ -> x) fx  (pure y) = fx 

associatività

liftA2 id   (liftA2 (\x y z -> f x y z) fx fy) fz = 
liftA2 (flip id) fx (liftA2 (\y z x -> f x y z) fy fz) 

naturalità

liftA2 (\x y -> o (f x) (g y)) fx fy = liftA2 o (fmap f fx) (fmap g fy) 

Non è immediatamente evidente che questi sono sufficienti a coprire la relazione tra fmap e Applicative s' pure e liftA2. Vediamo se possiamo dimostrare dalle leggi di cui sopra che

fmap f fx = liftA2 id (pure f) fx 

Inizieremo lavorando su fmap f fx. Tutti i seguenti sono equivalenti.

fmap f fx 
liftA2 (\x _ -> x) (fmap f fx) (  pure y)  -- by right identity 
liftA2 (\x _ -> x) (fmap f fx) ( id (pure y))  -- id x = x by definition 
liftA2 (\x _ -> x) (fmap f fx) (fmap id (pure y))  -- fmap id = id (Functor law) 
liftA2 (\x y -> (\x _ -> x) (f x) (id y)) fx (pure y) -- by naturality 
liftA2 (\x _ -> f x     ) fx (pure y) -- apply constant function 

A questo punto abbiamo scritto fmap in termini di liftA2, pure e qualsiasi y; fmap è interamente determinato dalle leggi di cui sopra. Il resto della prova non ancora provata è lasciato dall'autore irresoluto come esercizio per il lettore determinato.

Answer 2

Per il libro online, Learn You A Haskell:Functors, Applicative Functors and Monoids, le leggi del Codice di applicazione sono in sequenza ma riorganizzate per motivi di formattazione; tuttavia, sto facendo questo modificabile messaggio comunità dal momento che sarebbe utile se qualcuno potesse incorporare derivazioni:

identity]    v = pure id <*> v 
homomorphism]  pure (f x) = pure f <*> pure x 
interchange] u <*> pure y = pure ($ y) <*> u 
composition] u <*> (v <*> w) = pure (.) <*> u <*> v <*> w 

Nota:

function composition] (.) = (a->b) -> (b->c) -> (a->c) 
application operator] $ = (a->b) -> a -> b 

Found a treatment on Reddit