Czy prawa funktora udowadniają całkowitą ochronę struktury?

Question

W dokumentacji dla Data.Functor następujące dwa są określone jako prawa funktora, do których mają się stosować wszystkie funktory.

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

Droga moja intuicja mówi mi funktory powinien pracować jest to, że powinny one być „struktura zachowania”, czyli innymi słowy, jeśli masz funkcję f :: a -> b i to odwrotność g :: b -> a następnie

fmap f . fmap g == id 

Nie byłem w stanie wymyślić implementacji fmap, która byłaby zgodna z pierwszymi dwoma prawami i naruszała drugą, ale to nie jest żaden dowód. Czy ktoś może mnie oświecić?

Answer 1

Właściwie swoją „trzecią” Prawo funktor wynika bezpośrednio z faktycznym prawem funktorów oraz fakt, że f . g ≡ id:

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

A to nie wszystko: Haskell zapewnia, że ​​jeśli pierwsza zasada odnosi się do Functor instancji, a następnie drugi również posiada (jest to darmowe twierdzenie dla typu fmap). To znaczy. musisz udowodnić tylko prawo fmap id ≡ id dla swojej instancji Functor, aby upewnić się, że jest poprawna.