Chciałbym zaproponować bardziej systematyczne podejście do odpowiedzi na to pytanie, a także pokazać przykłady, w których nie stosuje się żadnych specjalnych sztuczek, takich jak „najniższe” wartości, nieskończone typy danych lub cokolwiek podobnego.
Kiedy konstruktory typów nie mają instancji klas typów?
Zasadniczo istnieją dwa powody, dla których konstruktor typów może nie mieć instancji określonej klasy typu:
- Nie można zaimplementować sygnatur typu wymaganych metod z klasy typu.
- Może implementować podpisy typu, ale nie może spełniać wymaganych praw.
Przykłady pierwszego rodzaju są łatwiejsze niż przykłady drugiego rodzaju, ponieważ w przypadku pierwszego rodzaju wystarczy sprawdzić, czy można zaimplementować funkcję z danym typem podpisu, natomiast w przypadku drugiego rodzaju musimy udowodnić, że nie ma implementacji mógłby ewentualnie spełniać prawa.
Konkretne przykłady
Jest to kontrafunkcjonariusz, a nie funktor, w odniesieniu do parametru type a, ponieważ aw pozycji przeciwstawnej. Niemożliwe jest wdrożenie funkcji z podpisem typu (a -> b) -> F z a -> F z b.
Konstruktor typów, który nie jest zgodnym z prawem funktorem, mimo że fmapmożna zaimplementować podpis typu :
data Q a = Q(a -> Int, a)
fmap :: (a -> b) -> Q a -> Q b
fmap f (Q(g, x)) = Q(\_ -> g x, f x) -- this fails the functor laws!
Ciekawy aspekt tego przykładu jest to, że można wdrożyć fmapod odpowiedniego typu, chociaż Fnie może być ewentualnie funktor ponieważ wykorzystuje aw kontrawariantny pozycji. Ta implementacja fmappokazana powyżej jest myląca - mimo że ma prawidłową sygnaturę typu (uważam, że jest to jedyna możliwa implementacja tego typu sygnatury), prawa funktora nie są spełnione. Na przykład fmap id≠ id, ponieważ let (Q(f,_)) = fmap id (Q(read,"123")) in f "456"jest 123, ale let (Q(f,_)) = id (Q(read,"123")) in f "456"jest 456.
W rzeczywistości Fjest tylko profesorem - nie jest ani funktorem, ani contrafunctor.
Zgodny z prawem funktor, który nie ma zastosowania, ponieważ purenie można zaimplementować podpisu typu : weź monadę Writer (a, w)i usuń ograniczenie, które wpowinno być monoidem. Wówczas niemożliwe jest skonstruowanie wartości typu (a, w)na podstawie a.
Funktora że nie jest aplikacyjnych , ponieważ podpis typu <*>nie mogą być realizowane: data F a = Either (Int -> a) (String -> a).
Funktor, który nie jest zgodny z prawem, mimo że można zastosować metody klasy typu:
data P a = P ((a -> Int) -> Maybe a)
Konstruktor typów Pjest funktorem, ponieważ używa atylko w pozycjach kowariantnych.
instance Functor P where
fmap :: (a -> b) -> P a -> P b
fmap fab (P pa) = P (\q -> fmap fab $ pa (q . fab))
Jedyną możliwą implementacją podpisu typu <*>jest funkcja, która zawsze zwraca Nothing:
(<*>) :: P (a -> b) -> P a -> P b
(P pfab) <*> (P pa) = \_ -> Nothing -- fails the laws!
Ale ta implementacja nie spełnia prawa tożsamości dla funktorów aplikacyjnych.
- Funktor, który
Applicativenie jest,Monad ponieważ bindnie można zaimplementować podpisu typu
Nie znam takich przykładów!
- Funktor,
Applicativeale nie jest tak,Monad ponieważ prawa nie mogą być spełnione, nawet jeśli bindmożna zaimplementować podpis typu .
Ten przykład wywołał sporo dyskusji, więc można śmiało powiedzieć, że udowodnienie poprawności tego przykładu nie jest łatwe. Ale kilka osób zweryfikowało to niezależnie różnymi metodami. Zobacz Is `data PoE a = Empty | Sparować monadę? do dodatkowej dyskusji.
data B a = Maybe (a, a)
deriving Functor
instance Applicative B where
pure x = Just (x, x)
b1 <*> b2 = case (b1, b2) of
(Just (x1, y1), Just (x2, y2)) -> Just((x1, x2), (y1, y2))
_ -> Nothing
Dość trudne jest udowodnienie, że nie ma zgodnej z prawem Monadinstancji. Przyczyną nie-monadycznego zachowania jest to, że nie ma naturalnego sposobu implementacji, bindkiedy funkcja f :: a -> B bmoże zwrócić Nothinglub Justdla różnych wartości a.
Być może bardziej zrozumiałe jest rozważenie Maybe (a, a, a), które również nie jest monadą, i próba wdrożenia jointego. Okaże się, że nie ma intuicyjnie rozsądnego sposobu wdrożenia join.
join :: Maybe (Maybe (a, a, a), Maybe (a, a, a), Maybe (a, a, a)) -> Maybe (a, a, a)
join Nothing = Nothing
join Just (Nothing, Just (x1,x2,x3), Just (y1,y2,y3)) = ???
join Just (Just (x1,x2,x3), Nothing, Just (y1,y2,y3)) = ???
-- etc.
W przypadkach wskazanych przez ???wydaje się jasne, że nie możemy wytwarzać Just (z1, z2, z3)w żaden rozsądny i symetryczny sposób z sześciu różnych wartości typu a. Z pewnością moglibyśmy wybrać dowolny arbitralny podzbiór tych sześciu wartości - na przykład zawsze przyjmujemy pierwszą niepustą Maybe- ale to nie spełniałoby praw monady. Powrót nie Nothingbędzie również zgodny z prawem.
- Drzewiasta struktura danych, która nie jest monadą, mimo że ma asocjatywność,
bindale nie spełnia praw tożsamości.
Zwykła monada drzewiasta (lub „drzewo z gałęziami w kształcie funktora”) jest zdefiniowana jako
data Tr f a = Leaf a | Branch (f (Tr f a))
Jest to wolna monada nad funktorem f. Kształt danych jest drzewem, w którym każdy punkt rozgałęzienia jest „funktorem” poddrzewa. Standardowe drzewo binarne można uzyskać za pomocą type f a = (a, a).
Jeśli zmodyfikujemy tę strukturę danych, tworząc również liście w kształcie funktora f, otrzymamy coś, co nazywam „semimonadą” - ma ono bindspełnienie praw natury i asocjatywności, ale jej puremetoda nie spełnia jednego z praw tożsamości. „Semimonady to półgrupy w kategorii endofunkcji, w czym problem?” To jest klasa typu Bind.
Dla uproszczenia definiuję joinmetodę zamiast bind:
data Trs f a = Leaf (f a) | Branch (f (Trs f a))
join :: Trs f (Trs f a) -> Trs f a
join (Leaf ftrs) = Branch ftrs
join (Branch ftrstrs) = Branch (fmap @f join ftrstrs)
Szczepienie gałęzi jest standardowe, ale szczepienie liści jest niestandardowe i powoduje Branch . Nie stanowi to problemu dla prawa o stowarzyszeniu, ale łamie jedno z praw dotyczących tożsamości.
Kiedy typy wielomianowe mają instancje monad?
Żaden z funktorów Maybe (a, a)i Maybe (a, a, a)może być udzielona legalnemu Monadinstancji, choć są oczywiście Applicative.
Te funktory nie mają żadnych sztuczek - żadnych Voidani bottomnigdzie, żadnych trudnych lenistw / ścisłości, żadnych nieskończonych struktur i żadnych ograniczeń klasowych. ApplicativePrzykład całkowicie standardowy. Funkcje returni bindmogą być zaimplementowane dla tych funktorów, ale nie spełniają praw monady. Innymi słowy, te funktory nie są monadami, ponieważ brakuje konkretnej struktury (ale nie jest łatwo zrozumieć, czego dokładnie brakuje). Na przykład niewielka zmiana funktora może przekształcić go w monadę: data Maybe a = Nothing | Just ajest monadą. Kolejnym podobnym funktorem data P12 a = Either a (a, a)jest także monada.
Konstrukcje monad wielomianowych
Ogólnie rzecz biorąc, oto niektóre konstrukcje, które produkują zgodne Monadz prawem typy wielomianowe. We wszystkich tych konstrukcjach Mjest monada:
type M a = Either c (w, a)gdzie wjest jakikolwiek monoidtype M a = m (Either c (w, a))gdzie mjest dowolna monada i wdowolna monoidtype M a = (m1 a, m2 a)gdzie m1i m2są dowolne monadytype M a = Either a (m a)gdzie mjest jakakolwiek monada
Pierwsza konstrukcja to WriterT w (Either c)druga konstrukcja WriterT w (EitherT c m). Trzecia konstrukcja jest produktem monad pure @Mskładającym się z komponentów : jest definiowana jako produkt składający się z pure @m1i pure @m2, i join @Mjest definiowany przez pominięcie danych między produktami (np. m1 (m1 a, m2 a)Jest odwzorowany m1 (m1 a)przez pominięcie drugiej części krotki):
join :: (m1 (m1 a, m2 a), m2 (m1 a, m2 a)) -> (m1 a, m2 a)
join (m1x, m2x) = (join @m1 (fmap fst m1x), join @m2 (fmap snd m2x))
Czwarta konstrukcja jest zdefiniowana jako
data M m a = Either a (m a)
instance Monad m => Monad M m where
pure x = Left x
join :: Either (M m a) (m (M m a)) -> M m a
join (Left mma) = mma
join (Right me) = Right $ join @m $ fmap @m squash me where
squash :: M m a -> m a
squash (Left x) = pure @m x
squash (Right ma) = ma
Sprawdziłem, czy wszystkie cztery konstrukcje produkują legalne monady.
I przypuszczać, że nie istnieją żadne inne zbudowania dla wielomianu monad. Na przykład funktor Maybe (Either (a, a) (a, a, a, a))nie jest uzyskiwany przez żadną z tych konstrukcji, a zatem nie jest monadyczny. Jednak Either (a, a) (a, a, a)jest monadycznego ponieważ jest izomorficzna z produktem trzech monad a, aoraz Maybe a. Ponadto Either (a,a) (a,a,a,a)jest monadyczny, ponieważ jest izomorficzny w stosunku do produktu ai Either a (a, a, a).
Cztery powyższe konstrukcje pozwolą nam uzyskać dowolną sumę dowolnej liczby produktów dowolnej liczby a, na przykład Either (Either (a, a) (a, a, a, a)) (a, a, a, a, a))i tak dalej. Wszystkie tego typu konstruktory będą miały (przynajmniej jedną) Monadinstancję.
Oczywiście okaże się, jakie przypadki użycia mogą istnieć dla takich monad. Inną kwestią jest to, że Monadprzypadki wyprowadzone za pomocą konstrukcji 1-4 nie są na ogół wyjątkowe. Na przykład, konstruktorowi typu type F a = Either a (a, a)można nadać Monadinstancję na dwa sposoby: przez konstrukcję 4 za pomocą monady (a, a)i przez konstrukcję 3 za pomocą izomorfizmu typu Either a (a, a) = (a, Maybe a). Znów znalezienie przypadków użycia dla tych implementacji nie jest od razu oczywiste.
Pozostaje pytanie - biorąc pod uwagę arbitralny wielomianowy typ danych, jak rozpoznać, czy ma on Monadinstancję. Nie wiem, jak udowodnić, że nie ma innych konstrukcji monad wielomianowych. Nie sądzę, aby jak dotąd istniała jakaś teoria odpowiadająca na to pytanie.
* -> *), dla którego nie ma odpowiedniegofmap?