Dobre przykłady Not a Functor / Functor / Applicative / Monad?

Wyjaśniając komuś, czym jest klasa X, staram się znaleźć dobre przykłady struktur danych, które są dokładnie X.

Proszę o przykłady:

• Konstruktor typów, który nie jest Functorem.
• Konstruktor typów, który jest Functorem, ale nie ma zastosowania.
• Konstruktor typów, który jest aplikacyjny, ale nie jest monadą.
• Konstruktor typów, który jest Monadą.

Myślę, że wszędzie jest wiele przykładów Monady, ale dobry przykład Monady z pewnym odniesieniem do poprzednich przykładów może uzupełnić obraz.

Szukam przykładów, które byłyby do siebie podobne, różniąc się tylko aspektami ważnymi dla przynależności do określonej klasy typów.

Gdyby udało się podkraść przykład Strzałki gdzieś w tej hierarchii (czy to między Applicative i Monad?), To też byłoby świetnie!

Konstruktor typów, który nie jest Functorem:

newtype T a = T (a -> Int)

Można z niego zrobić funktor kontrowariantny, ale nie funktor (kowariantny). Spróbuj pisać, fmapa nie powiedzie się. Zauważ, że przeciwna wersja funktora jest odwrócona:

fmap      :: Functor f       => (a -> b) -> f a -> f b
contramap :: Contravariant f => (a -> b) -> f b -> f a

Konstruktor typów, który jest funktorem, ale nie ma zastosowania:

Nie mam dobrego przykładu. Jest Const, ale idealnie chciałbym konkretnego nie-monoida i nie mogę myśleć o żadnym. Wszystkie typy są w zasadzie numeryczne, wyliczenia, produkty, sumy lub funkcje, kiedy do tego dojdzie. Możesz zobaczyć poniżej pigworker, a ja nie zgadzam się co do tego, czy Data.Voidjest Monoid;

instance Monoid Data.Void where
    mempty = undefined
    mappend _ _ = undefined
    mconcat _ = undefined

Ponieważ _|_jest to wartość prawna w Haskell i faktycznie jedyna wartość prawna Data.Void, jest to zgodne z zasadami Monoid. Nie jestem pewien, co unsafeCoercema z tym wspólnego, ponieważ nie ma już gwarancji, że twój program nie naruszy semantyki Haskell, gdy tylko użyjesz jakiejkolwiek unsafefunkcji.

Zobacz Wiki Haskell, aby znaleźć artykuł na temat dolnej ( link ) lub niebezpiecznych funkcji ( link ).

Zastanawiam się, czy możliwe jest stworzenie takiego konstruktora typu przy użyciu bogatszego systemu typu, takiego jak Agda lub Haskell z różnymi rozszerzeniami.

Konstruktor typów, który jest aplikacją, ale nie monadą:

newtype T a = T {multidimensional array of a}

Możesz zrobić z niego aplikację, używając czegoś takiego:

mkarray [(+10), (+100), id] <*> mkarray [1, 2]
  == mkarray [[11, 101, 1], [12, 102, 2]]

Ale jeśli uczynisz go monadą, możesz uzyskać niedopasowanie wymiarów. Podejrzewam, że takie przykłady są rzadkie w praktyce.

Konstruktor typów, który jest Monadą:

[]

O strzałkach:

Pytanie o to, gdzie leży strzała w tej hierarchii, jest jak pytanie, jaki jest kształt „czerwonego”. Zwróć uwagę na rodzaj niedopasowania:

Functor :: * -> *
Applicative :: * -> *
Monad :: * -> *

ale,

Arrow :: * -> * -> *

Mój styl może być ciasny przez mój telefon, ale proszę bardzo.

newtype Not x = Kill {kill :: x -> Void}

nie może być Functorem. Gdyby tak było, mielibyśmy

kill (fmap (const ()) (Kill id)) () :: Void

a Księżyc byłby zrobiony z zielonego sera.

W międzyczasie

newtype Dead x = Oops {oops :: Void}

jest funktorem

instance Functor Dead where
  fmap f (Oops corpse) = Oops corpse

ale nie mogą mieć zastosowania, inaczej byśmy mieli

oops (pure ()) :: Void

a zielony byłby zrobiony z sera księżycowego (co może się zdarzyć, ale dopiero później wieczorem).

(Dodatkowa uwaga: Voidponieważ w Data.Voidjest pustym typem danych. Jeśli spróbujesz użyć, undefinedaby udowodnić, że jest to Monoid, użyję, unsafeCoerceaby udowodnić, że nie jest.)

Radośnie,

newtype Boo x = Boo {boo :: Bool}

ma zastosowanie na wiele sposobów, np. tak, jak chciałby to Dijkstra,

instance Applicative Boo where
  pure _ = Boo True
  Boo b1 <*> Boo b2 = Boo (b1 == b2)

ale to nie może być monada. Aby zobaczyć, dlaczego nie, zwróć uwagę, że powrót musi następować w sposób ciągły Boo Truelub Boo Falseodtąd

join . return == id

nie może być w stanie utrzymać.

O tak, prawie zapomniałem

newtype Thud x = The {only :: ()}

jest Monadą. Skręć swój własny.

Samolot do złapania ...

Uważam, że w innych odpowiedziach pominięto kilka prostych i powszechnych przykładów:

Konstruktor typów, który jest Functorem, ale nie aplikacją. Prostym przykładem jest para:

instance Functor ((,) r) where
    fmap f (x,y) = (x, f y)

Ale nie ma sposobu, jak zdefiniować jego Applicativeinstancję bez nakładania dodatkowych ograniczeń r. W szczególności nie ma możliwości zdefiniowania pure :: a -> (r, a)arbitralności r.

Konstruktor typów, który jest aplikacyjny, ale nie jest monadą. Dobrze znanym przykładem jest ZipList . (Jest to newtypeopakowanie, które zawija listy i zapewnia Applicativedla nich różne wystąpienia).

fmapjest zdefiniowany w zwykły sposób. Ale purei <*>są zdefiniowane jako

pure x                    = ZipList (repeat x)
ZipList fs <*> ZipList xs = ZipList (zipWith id fs xs)

puretworzy więc nieskończoną listę, powtarzając podaną wartość, i <*>zamyka listę funkcji z listą wartości - stosuje i-tą funkcję do i-tego elementu. (Standard <*>na []tworzy wszystkie możliwe kombinacje zastosowania i- tej funkcji do j-tego elementu.) Ale nie ma rozsądnego sposobu na zdefiniowanie monady (zobacz ten post ).

Jak strzałki pasują do hierarchii funktorów / aplikacji / monad? Zobacz idiomy są nieświadome, strzały są drobiazgowe, monady są rozwiązłe przez Sama Lindleya, Philipa Wadlera, Jeremy Yallopa. MSFP 2008. (Nazywają idiomy funktorów aplikacyjnych .) Streszczenie:

Powracamy do związku między trzema pojęciami obliczeń: monadami Moggiego, strzałami Hughesa i idiomami McBride'a i Patersona (zwanymi także funktorami aplikacyjnymi). Pokazujemy, że idiomy są równoważne strzałkom spełniającym typ izomorfizmu A ~> B = 1 ~> (A -> B) oraz że monady są równoważne strzałkom spełniającym typ izomorfizmu A ~> B = A -> (1 ~ > B). Ponadto idiomy osadzone w strzałach i strzałki osadzone w monadach.

Dobrym przykładem konstruktora typów, który nie jest funktorem, jest Set: Nie można zaimplementować fmap :: (a -> b) -> f a -> f b, ponieważ bez dodatkowego ograniczenia Ord bnie można skonstruować f b.

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:

1. Nie można zaimplementować sygnatur typu wymaganych metod z klasy typu.
2. 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

• Konstruktor typów, który nie może mieć instancji funktora, ponieważ nie można zaimplementować typu:

  data F z a = F (a -> z)

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:

1. type M a = Either c (w, a)gdzie wjest jakikolwiek monoid
2. type M a = m (Either c (w, a))gdzie mjest dowolna monada i wdowolna monoid
3. type M a = (m1 a, m2 a)gdzie m1i m2są dowolne monady
4. type 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.