2014-05-15 13 views
8

Nella documentazione per Data.Functor i seguenti due sono indicati come leggi del funtore, a cui tutti i funtori devono attenersi.Le leggi del funtore dimostrano la completa conservazione della struttura?

fmap id == id 
fmap (f . g) == fmap f . fmap g 

Il modo in cui la mia intuizione mi dice funtori dovrebbero lavorare è che essi dovrebbero essere "struttura preservare", o in altre parole, se si dispone di una funzione f :: a -> b ed è inversa g :: b -> a poi

fmap f . fmap g == id 

Non sono stato in grado di realizzare un'implementazione di fmap che aderirebbe alle prime due leggi e violerebbe la seconda, ma non è affatto una prova. Qualcuno può illuminarmi?

+0

+1 Sono stato alle prese con domande simili ultimamente. C'è una cosa che mi infastidisce con questa formulazione intuitiva: per quanto riguarda le funzioni senza inversione? Sicuramente 'fmap (const" Foo ")' è una struttura che preserva anche in un certo senso? – duplode

+0

Sì, ma non è possibile usare 'const" Foo "' per provare la legge vera - devi scegliere un'altra funzione. Non sto dicendo che i funtori sono validi solo per i tipi di funzioni che la legge racchiude. – kqr

+0

@duplode immaginare un albero 'albero dati a = foglia | Nodo a [Albero a] '. Quando parliamo di "struttura" di 't :: Tree a' pensiamo a quanti sottoalberi ha ciascun nodo e come sono disposti questi sottoalberi. Quindi potresti dire che siamo interessati a 't' con _qualcosa nei suoi nodi_. E infatti possiamo catturarlo con 'fmap (const()) t'. – fizruk

risposta

13

In realtà, la tua legge "terzo" funtore deriva direttamente dalle leggi attuali funtore e il fatto che f . g ≡ id:

fmap f . fmap g ≡ fmap (f . g) ≡ fmap id ≡ id 

E c'è di più: Haskell assicura che se prima legge vale per Functor esempio, allora la seconda detiene anche (questo è un teorema gratuito per il tipo di fmap). Cioè devi dimostrare solo la legge fmap id ≡ id per l'istanza Functor per assicurarti che sia valida.

+0

Quando 'f. g ≡ id', entrambe le funzioni 'f' e' g' hanno un termine matematico che descrive la loro relazione? (Penso di aver letto l'isomorfismo da qualche parte, ma non ne sono sicuro.) – Sibi

+1

@Sibi: perché, sì, 'f' è un inverso a sinistra di' g' e 'g' è un inverso a destra di' f'. Ciò non implica l'isomorfismo del dominio e del codominio di nessuna delle funzioni, ad esempio 'show :: Int -> String' ha' read' come inverso a sinistra, sebbene 'Int' abbia ovviamente una cardinalità più piccola di' String'. – leftaroundabout

+7

@Sibi Si noti che 'f. g ≡ id' non implica 'g. f ≡ id'. Tuttavia, se è il caso allora entrambe le funzioni sono chiamate _ "isomorfismi" _. Altrimenti, 'f' è chiamato _" retraction "_ (o _" left inverse di 'g'" _) e 'g' è chiamato _" section "_ (o _" right inverse di 'f'" _). – fizruk

Problemi correlati