Twierdzono, że newtype T a = T (a -> Int) jest konstruktorem typu, który nie jest funktorem (ale jest przeciwwariantowym funktorem). Jak to? Albo co to jest contravariant functor (skąd zakładam, że będzie oczywiste, dlaczego nie można go uczynić normalnym funktorem)?Pokazywanie, że `nowy typ T a = T (a -> Int)` jest konstruktorem typów, który nie jest funktorem
Biorąc
newtype T a = T (a -> Int)
spróbujmy zbudować instancję Contravariant dla tego typu danych.
Oto typeclass w pytaniu:
class Contravariant f where
contramap :: (a -> b) -> f b -> f a
Zasadniczo contramap jest zbliżona do fmap, ale zamiast podnoszenia funkcję a -> b do f a -> f b, że unosi go do f b -> f a.
Zacznijmy pisząc wystąpienie ...
instance Contravariant T where
contramap g (T f) = ?
Zanim wypełnić ?, pomyślmy o tym, co rodzaje g i f są:
g :: a -> b
f :: b -> Int
I dla jasności, mamy może również wspomnieć, że
f a ~ T (a -> Int)
f b ~ T (b -> Int)
Tak więc możemy wypełnić ? następująco:
instance Contravariant T where
contramap g (T f) = T (f . g)
Być super pedantyczny, można zmienić nazwę g jako aToB i f jak bToInt.
instance Contravariant T where
contramap aToB (T bToInt) = T (bToInt . aToB)
Powodem można napisać instancji Contravariant dla T a sprowadza się do faktu, że a jest w kontrawariantny pozycji w T (a -> Int). Najlepszym sposobem, aby przekonać się, że T a nie jest Functor, jest próba (i niepowodzenie) samodzielnego napisania instancji Functor.
Załóżmy, że T jest funktorem. Następnie mamy
fmap :: (a -> b) -> T a -> T b
Teraz spróbujmy go wdrożyć.
instance Functor T where
fmap f (T g) = T $ \x -> _y
Oczywiście zaczniemy od czegoś takiego, i połączyć wartości f, g i x jakoś obliczyć wartość y który jest z prawej typu. Jak możemy to zrobić? Zauważcie, że nazwałem to _y, co mówi GHC, że potrzebuję pomocy w ustaleniu, co tam umieścić. Co ma do powiedzenia GHC?
<interactive>:7:28: error:
• Found hole: _y :: Int
Or perhaps ‘_y’ is mis-spelled, or not in scope
• In the expression: _y
In the second argument of ‘($)’, namely ‘\ x -> _y’
In the expression: T $ \ x -> _y
• Relevant bindings include
x :: b (bound at <interactive>:7:23)
g :: a -> Int (bound at <interactive>:7:13)
f :: a -> b (bound at <interactive>:7:8)
fmap :: (a -> b) -> T a -> T b (bound at <interactive>:7:3)
Teraz wiemy, jakie rodzaje wszystkiego są istotne, prawda? Musimy zwrócić Int jakoś, a co musimy zbudować go z to:
x :: b
g :: a -> Int
f :: a -> b
Dobrze, dobrze, jedyne co mamy, które mogą ewentualnie tworzyć Int jest g, więc niech wypełnić, że, pozostawiając g argumentacja puste zapytać gHC, aby uzyskać pomoc:
instance Functor T where
fmap f (T g) = T $ \x -> g _y
<interactive>:7:31: error:
• Found hole: _y :: a
Where: ‘a’ is a rigid type variable bound by
the type signature for:
fmap :: forall a b. (a -> b) -> T a -> T b
at <interactive>:7:3
Or perhaps ‘_y’ is mis-spelled, or not in scope
• In the first argument of ‘g’, namely ‘(_y)’
In the expression: g (_y)
In the second argument of ‘($)’, namely ‘\ x -> g (_y)’
• Relevant bindings include
x :: b (bound at <interactive>:7:23)
g :: a -> Int (bound at <interactive>:7:13)
f :: a -> b (bound at <interactive>:7:8)
fmap :: (a -> b) -> T a -> T b (bound at <interactive>:7:3)
Ok, możemy przewidzieć to sami: zadzwonić g musimy wartość typu a od gdzieś. Ale nie mamy żadnych wartości typu a w zakresie, i nie mamy żadnych funkcji, które zwracają wartość typu a albo! Utknęliśmy: niemożliwe jest stworzenie wartości, jakiej oczekujemy teraz, mimo że na każdym kroku zrobiliśmy jedyną możliwą rzecz: nie ma niczego, co moglibyśmy zarchiwizować i spróbować inaczej.
Dlaczego tak się stało? Ponieważ jeśli dam ci funkcję typu a -> Int i powiem "ale przy okazji, oto funkcja od a -> b, proszę, zwróć mi funkcję z b -> Int zamiast", nie możesz faktycznie użyć funkcji od a -> b, ponieważ nikt kiedykolwiek daje ci a s, aby zadzwonić! Gdybym zamiast tego dał ci funkcję z b -> a, byłoby to pomocne, prawda? Można wtedy utworzyć funkcję z b -> Int, najpierw wywołując funkcję b -> a, aby uzyskać a, a następnie wywołując oryginalną funkcję a -> Int, aby uzyskać żądaną wartość Int.
Na tym polega przeciwwirusowy funktor: odwracamy strzałkę w funkcji przekazywanej do fmap, dzięki czemu może ona fmapować rzeczy, które "potrzebujesz" (argumenty funkcji) zamiast rzeczy, które "masz" (konkretne wartości, powrót wartości funkcji itp.).
Poza tym: Powiedziałem wcześniej, że zrobiliśmy "jedyną możliwą rzecz" na każdym kroku, co było trochę kłamstwem. Nie możemy zbudować Int z f, g i x, ale oczywiście możemy wymyślić różne rodzaje liczb z powietrza.Nie wiemy nic o typie b, więc nie możemy uzyskać Int pochodzącej z niego w jakiś sposób, ale moglibyśmy powiedzieć "niech zawsze zwróci zero", a to technicznie spełnia funkcję sprawdzania typu:
instance Functor T where
fmap f (T g) = T $ const 0
Oczywiście wygląda to całkiem źle, ponieważ wygląda na to, że f i g powinny być dość ważne i ignorujemy je! Ale to kontrole typu, więc jesteśmy w porządku, prawda?
Nie, to narusza jedno z praw funktora:
fmap id = id
Możemy udowodnić to dość łatwo:
fmap id (T $ const 5) = (T $ const 0) /= (T $ const 5)
A teraz naprawdę mieć próbował wszystko: jedynym sposobem mamy zbudowanie modelu Int bez korzystania z naszego typu wcale nie jest możliwe, a wszystkie takie zastosowania będą izomorficzne z używaniem const, które będą naruszać prawa Funktorów.
Oto kolejny punkt widzenia. Jak pokazał liminalisht, T to Contravariant.Co możemy powiedzieć o typach, które są zarówno kowariantne, jak i contravariant?
import Data.Void
change1, change1', change2 :: (Functor f, Contravariant f) => f a -> f b
change1 = contramap (const()) . fmap (const())
change1' = (() >$) . (() <$)
change2 = fmap absurd . contramap absurd
Pierwsze dwie implementacje są zasadniczo takie same (change1' jest optymalizacja change1); każdy z nich wykorzystuje fakt, że () jest "obiektem terminalowym" Hask. change2 zamiast tego wykorzystuje fakt, że Void jest "obiektem początkowym".
Każda z tych funkcji zastępuje wszystkie a s w f a z b s bez znajomości czegokolwiek o a, b, lub relacje między nimi, pozostawiając wszystko inne samo. Prawdopodobnie powinno być jasne, że oznacza to, że f a tak naprawdę nie zależy od a. To znaczy, parametr f musi być fantomowy. To jest , a nie przypadek dla, więc nie może być również kowariantny.