Gute Beispiele für Not a Functor / Functor / Applicative / Monad?

209

Während ich jemandem erkläre, was eine Typklasse X ist, bemühe ich mich, gute Beispiele für Datenstrukturen zu finden, die genau X sind.

Also bitte ich um Beispiele für:

  • Ein Typkonstruktor, der kein Functor ist.
  • Ein Typkonstruktor, der ein Functor ist, aber nicht anwendbar.
  • Ein Typkonstruktor, der anwendbar ist, aber keine Monade.
  • Ein Typkonstruktor, der eine Monade ist.

Ich denke, es gibt überall viele Beispiele für Monaden, aber ein gutes Beispiel für Monaden mit einer gewissen Beziehung zu früheren Beispielen könnte das Bild vervollständigen.

Ich suche nach Beispielen, die einander ähnlich wären und sich nur in Aspekten unterscheiden, die für die Zugehörigkeit zur jeweiligen Typklasse wichtig sind.

Wenn es gelingen könnte, irgendwo in dieser Hierarchie ein Beispiel für Arrow zu finden (liegt es zwischen Applicative und Monad?), Wäre das auch großartig!

Rotsor
quelle
4
Ist es möglich, einen Typkonstruktor ( * -> *) zu erstellen, für den es keinen geeigneten gibt fmap?
Owen
1
Owen, ich denke a -> Stringist kein Funktor.
Rotsor
3
@Rotsor @Owen a -> Stringist ein mathematischer Funktor, aber kein Haskell Functor, um es klar zu sagen .
J. Abrahamson
@J. Abrahamson, inwiefern ist es dann ein mathematischer Funktor? Sprechen Sie über die Kategorie mit umgekehrten Pfeilen?
Rotsor
3
Für Leute, die nicht wissen, hat ein kontravarianter Funktor eine fmap vom Typ(a -> b) -> f b -> f a
AJFarmar

Antworten:

100

Ein Typkonstruktor, der kein Functor ist:

newtype T a = T (a -> Int)

Sie können daraus einen kontravarianten Funktor machen, aber keinen (kovarianten) Funktor. Versuchen Sie zu schreiben fmapund Sie werden scheitern. Beachten Sie, dass die kontravariante Funktorversion umgekehrt ist:

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

Ein Typkonstruktor, der ein Funktor ist, aber nicht anwendbar:

Ich habe kein gutes Beispiel. Es gibt Const, aber im Idealfall hätte ich gerne ein konkretes Nicht-Monoid und mir fällt keines ein. Alle Typen sind im Grunde genommen numerisch, Aufzählungen, Produkte, Summen oder Funktionen, wenn Sie darauf eingehen. Sie können unten Schweinearbeiter sehen und ich bin nicht einverstanden darüber, ob Data.Voides sich um einen handelt Monoid;

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

Da dies _|_in Haskell ein rechtlicher Wert ist und tatsächlich der einzige rechtliche Wert von Data.Void, erfüllt dies die Monoid-Regeln. Ich bin mir nicht sicher, was unsafeCoercedamit zu tun hat, da Ihr Programm nicht mehr garantiert nicht gegen die Haskell-Semantik verstößt, sobald Sie eine unsafeFunktion verwenden.

Im Haskell-Wiki finden Sie einen Artikel unten ( Link ) oder unsichere Funktionen ( Link ).

Ich frage mich, ob es möglich ist, einen solchen Typkonstruktor mit einem umfangreicheren Typsystem wie Agda oder Haskell mit verschiedenen Erweiterungen zu erstellen.

Ein Typkonstruktor, der anwendbar, aber keine Monade ist:

newtype T a = T {multidimensional array of a}

Sie können daraus einen Antrag stellen, mit:

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

Wenn Sie es jedoch zu einer Monade machen, kann es zu einer Nichtübereinstimmung der Dimensionen kommen. Ich vermute, dass solche Beispiele in der Praxis selten sind.

Ein Typkonstruktor, der eine Monade ist:

[]

Über Pfeile:

Zu fragen, wo ein Pfeil auf dieser Hierarchie liegt, ist wie zu fragen, was für eine Form "rot" ist. Beachten Sie die Art der Nichtübereinstimmung:

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

aber,

Arrow :: * -> * -> *
Dietrich Epp
quelle
3
Gute Liste! Ich würde vorschlagen, etwas Einfacheres wie Either aals Beispiel für den letzten Fall zu verwenden, da es leichter zu verstehen ist.
Fuz
6
Wenn Sie immer noch nach einem Typkonstruktor suchen, der anwendbar ist, aber keine Monade, ist dies ein sehr häufiges Beispiel ZipList.
John L
23
_|_bewohnt jeden Typ in *, aber der Punkt Voidist, dass Sie sich nach hinten beugen müssen, um einen zu konstruieren, oder Sie haben seinen Wert zerstört. Aus diesem Grund handelt es sich nicht um eine Instanz von Enum, Monoid usw. Wenn Sie bereits eine haben, lasse ich Sie diese gerne zusammenfügen (geben Sie eine Semigroup) mempty, aber ich gebe keine Werkzeuge zum expliziten Konstruieren eines Wertes vom Typ Voidin void. Sie müssen die Waffe laden und auf Ihren Fuß richten und selbst den Abzug betätigen.
Edward KMETT
2
Pedantisch denke ich, dass Ihre Vorstellung von Cofunctor falsch ist. Das Dual eines Funktors ist ein Funktor, weil Sie sowohl den Eingang als auch den Ausgang umdrehen und am Ende genau das Gleiche erhalten. Der Begriff, den Sie suchen, ist wahrscheinlich "Contravariant Functor", was etwas anders ist.
Ben Millwood
1
@AlexVong: "Veraltet" -> Leute verwenden nur ein anderes Paket. Apropos "kontravarianter Funktor", nicht "Dual of Funktor", entschuldigen Sie die Verwirrung. In einigen Zusammenhängen habe ich gesehen, dass "Cofunctor" sich auf "kontravariante Funktoren" bezog, weil Funktoren sich selbst verdoppeln, aber es scheint nur verwirrend zu sein.
Dietrich Epp
87

Mein Stil kann durch mein Telefon beengt sein, aber hier geht es weiter.

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

kann kein Functor sein. Wenn es so wäre, hätten wir es getan

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

und der Mond würde aus grünem Käse bestehen.

inzwischen

newtype Dead x = Oops {oops :: Void}

ist ein Funktor

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

kann aber nicht anwendbar sein, oder wir hätten

oops (pure ()) :: Void

und Grün würde aus Mondkäse hergestellt (was tatsächlich passieren kann, aber erst später am Abend).

(Zusätzliche Anmerkung: Void, wie in Data.Voideinem leeren Datentyp Wenn Sie versuchen , zu verwenden. undefinedZu beweisen , es ist ein Monoid, ich werde verwenden unsafeCoercezu beweisen, dass es nicht ist.)

Freudig,

newtype Boo x = Boo {boo :: Bool}

ist in vielerlei Hinsicht anwendbar, z. B. wie Dijkstra es haben würde,

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

aber es kann keine Monade sein. Um zu sehen , warum nicht, beachten Sie, dass die Rückkehr sein muss ständig Boo Trueoder Boo False, und damit , dass

join . return == id

kann unmöglich halten.

Oh ja, ich hätte es fast vergessen

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

ist eine Monade. Roll deinen eigenen.

Flugzeug zu fangen ...

Schweinearbeiter
quelle
8
Die Leere ist leer! Jedenfalls moralisch.
Schweinearbeiter
9
Void ist ein Typ mit 0 Konstruktoren, nehme ich an. Es ist kein Monoid, weil es kein gibt mempty.
Rotsor
6
nicht definiert? Wie unhöflich! Leider ist unsafeCoerce (unsafeCoerce () <*> undefined) nicht (), daher gibt es im wirklichen Leben Beobachtungen, die gegen die Gesetze verstoßen.
Schweinearbeiter
5
In der üblichen Semantik, die genau eine Art von undefiniert toleriert, haben Sie völlig Recht. Es gibt natürlich auch andere Semantiken. Die Leere beschränkt sich nicht auf ein Submonoid im Gesamtfragment. Es ist auch kein Monoid in einer Semantik, die Ausfallarten unterscheidet. Wenn ich einen Moment mit einfacher als telefonischer Bearbeitung habe, werde ich klarstellen, dass mein Beispiel nur in einer Semantik funktioniert, für die es nicht genau eine Art von undefiniert gibt.
Schweinearbeiter
22
Viel Lärm um_|_
Landei
71

Ich glaube, die anderen Antworten haben einige einfache und häufige Beispiele übersehen:

Ein Typkonstruktor, der ein Functor, aber kein Applicative ist. Ein einfaches Beispiel ist ein Paar:

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

Es gibt jedoch keine Möglichkeit, die ApplicativeInstanz zu definieren, ohne zusätzliche Einschränkungen aufzuerlegen r. Insbesondere gibt es keine Möglichkeit, pure :: a -> (r, a)für eine beliebige zu definieren r.

Ein Typkonstruktor, der anwendbar ist, aber keine Monade.Ein bekanntes Beispiel ist ZipList . (Es ist eine newtype, die Listen umschließt und verschiedene ApplicativeInstanzen für sie bereitstellt .)

fmapwird wie gewohnt definiert. Aberpure und <*>sind definiert als

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

so pureschafft eine unendliche Liste von dem angegebenen Wert zu wiederholen, und <*>Reißverschluss eine Liste von Funktionen mit einer Liste von Werten - gilt i - ten Funktion i -te Element. (Der Standard <*>ein []erzeugt alle möglichen Kombinationen der Anwendung der i- ten Funktion auf j- te Element.) Es gibt jedoch keine sinnvolle Möglichkeit, eine Monade zu definieren (siehe diesen Beitrag ).


Wie passen Pfeile in die Funktor- / Anwendungs- / Monadenhierarchie? Sehen Redewendungen sind ahnungslos, Pfeile sind akribisch, Monaden sind von Sam Lindley, Philip Wadler und Jeremy Yallop promiskuitiv . MSFP 2008. (Sie nennen anwendbare Funktoren Idiome .) Die Zusammenfassung:

Wir überdenken die Verbindung zwischen drei Begriffen der Berechnung: Moggis Monaden, Hughes 'Pfeile und McBride- und Patersons Redewendungen (auch als anwendungsbezogene Funktoren bezeichnet). Wir zeigen, dass Redewendungen Pfeilen entsprechen, die den Typisomorphismus A ~> B = 1 ~> (A -> B) erfüllen, und dass Monaden Pfeilen entsprechen, die den Typisomorphismus A ~> B = A -> (1 ~) erfüllen > B). Ferner sind Redewendungen in Pfeile und Pfeile in Monaden eingebettet.

Petr Pudlák
quelle
1
So ((,) r)ist ein Funktor, der keine Anwendung ist; Dies liegt jedoch nur daran, dass Sie im Allgemeinen nicht purefür alle gleichzeitig definieren können r. Es ist daher eine Eigenart der sprachlichen Prägnanz, zu versuchen, eine (unendliche) Sammlung von anwendbaren Funktoren mit einer Definition von pureund zu definieren <*>; in diesem Sinne scheint es nichts mathematisch tief über dieses Gegenbeispiel zu sein , da für jeden Beton r, ((,) r) kann eine applicative Funktors gemacht werden. Frage: Können Sie sich einen CONCRETE-Funktor vorstellen, der nicht anwendbar ist?
George
1
Siehe stackoverflow.com/questions/44125484/… als Beitrag mit dieser Frage.
George
20

Ein gutes Beispiel für einen Typkonstruktor, der kein Funktor ist, ist Set: Sie können nicht implementieren fmap :: (a -> b) -> f a -> f b, da Sie ohne eine zusätzliche Einschränkung Ord bnicht konstruieren können f b.

Landei
quelle
16
Es ist eigentlich ein gutes Beispiel, da wir mathematisch wirklich gerne einen Funktor daraus machen würden.
Alexandre C.
21
@AlexandreC. Ich würde dem nicht zustimmen, es ist kein gutes Beispiel. Mathematisch gesehen bildet eine solche Datenstruktur einen Funktor. Die Tatsache, dass wir nicht implementieren können, fmapist nur ein Sprach- / Implementierungsproblem. Es ist auch möglich, sich Setin die Fortsetzungsmonade einzuwickeln , die daraus eine Monade mit allen Eigenschaften macht, die wir erwarten würden. Siehe diese Frage (obwohl ich nicht sicher bin, ob dies effizient durchgeführt werden kann).
Petr Pudlák
@PetrPudlak, wie ist das ein Sprachproblem? Gleichheit von bkann unentscheidbar sein, in diesem Fall können Sie nicht definieren fmap!
Turion
@Turion Entscheidbar und definierbar zu sein, sind zwei verschiedene Dinge. Zum Beispiel ist es möglich, Gleichheit für Lambda-Begriffe (Programme) korrekt zu definieren, obwohl es nicht möglich ist, sie durch einen Algorithmus zu entscheiden. In diesem Beispiel war dies jedenfalls nicht der Fall. Hier besteht das Problem darin, dass wir keine FunctorInstanz mit der OrdEinschränkung definieren können, dies jedoch möglicherweise mit einer anderen Definition Functoroder einer besseren Sprachunterstützung möglich ist. Tatsächlich ist es mit ConstraintKinds möglich , eine Typklasse zu definieren, die so parametrisiert werden kann.
Petr Pudlák
Selbst wenn wir die ordEinschränkung überwinden könnten, bedeutet die Tatsache, dass a Setkeine doppelten Einträge enthalten kann, dass fmapdies den Kontext verändern könnte. Dies verstößt gegen das Assoziativitätsgesetz.
John F. Miller
11

Ich möchte einen systematischeren Ansatz zur Beantwortung dieser Frage vorschlagen und Beispiele zeigen, die keine speziellen Tricks wie die "unteren" Werte oder unendlichen Datentypen oder ähnliches verwenden.

Wann haben Typkonstruktoren keine Typklasseninstanzen?

Im Allgemeinen gibt es zwei Gründe, warum ein Typkonstruktor möglicherweise keine Instanz einer bestimmten Typklasse hat:

  1. Die Typensignaturen der erforderlichen Methoden aus der Typklasse können nicht implementiert werden.
  2. Kann die Typensignaturen implementieren, aber die erforderlichen Gesetze nicht erfüllen.

Beispiele der ersten Art sind einfacher als Beispiele der zweiten Art, da wir für die erste Art nur prüfen müssen, ob eine Funktion mit einer bestimmten Typensignatur implementiert werden kann, während für die zweite Art nachgewiesen werden muss, dass keine Implementierung erfolgt könnte möglicherweise die Gesetze erfüllen.

Spezifische Beispiele

  • Ein Typkonstruktor, der keine Funktorinstanz haben kann, weil der Typ nicht implementiert werden kann:

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

Dies ist ein Kontrafunktor, kein Funktor, in Bezug auf den Typparameter a, weil ain einer kontravarianten Position. Es ist unmöglich, eine Funktion mit Typensignatur zu implementieren (a -> b) -> F z a -> F z b.

  • Ein Typkonstruktor, der kein rechtmäßiger Funktor ist , obwohl die Typensignatur von fmapimplementiert werden kann:

    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!

Der merkwürdige Aspekt dieses Beispiels ist, dass wir den richtigen Typ implementieren können , fmapobwohl wir Fmöglicherweise kein Funktor sein können, weil er ain einer kontravarianten Position verwendet wird. Diese fmapoben gezeigte Implementierung ist also irreführend - obwohl sie die richtige Typensignatur hat (ich glaube, dies ist die einzig mögliche Implementierung dieser Typensignatur), sind die Funktorgesetze nicht erfüllt. Zum Beispiel fmap idid, weil let (Q(f,_)) = fmap id (Q(read,"123")) in f "456"ist 123, aber let (Q(f,_)) = id (Q(read,"123")) in f "456"ist 456.

In der Tat Fist nur ein Profunctor, - es ist weder ein Funktor noch ein Kontrafunktor.

  • Ein rechtmäßiger Funktor, der nicht anwendbar ist, weil die Typensignatur von purenicht implementiert werden kann: Nehmen Sie die Writer-Monade (a, w)und entfernen Sie die Einschränkung, wdie ein Monoid sein sollte. Es ist dann unmöglich, einen Wert vom Typ (a, w)aus zu konstruieren a.

  • Ein Funktor, der nicht anwendbar ist, weil die Typensignatur von <*>nicht implementiert werden kann : data F a = Either (Int -> a) (String -> a).

  • Ein Funktor, der nicht rechtmäßig anwendbar ist , obwohl die Typklassenmethoden implementiert werden können:

    data P a = P ((a -> Int) -> Maybe a)

Der Typkonstruktor Pist ein Funktor, da er anur in kovarianten Positionen verwendet wird.

instance Functor P where
   fmap :: (a -> b) -> P a -> P b
   fmap fab (P pa) = P (\q -> fmap fab $ pa (q . fab))

Die einzig mögliche Implementierung der Typensignatur von <*>ist eine Funktion, die immer Folgendes zurückgibt Nothing:

 (<*>) :: P (a -> b) -> P a -> P b
 (P pfab) <*> (P pa) = \_ -> Nothing  -- fails the laws!

Diese Implementierung entspricht jedoch nicht dem Identitätsgesetz für anwendbare Funktoren.

  • Ein Funktor, der Applicativeaber kein ist ,Monad weil die Typensignatur von bindnicht implementiert werden kann.

Ich kenne keine solchen Beispiele!

  • Ein Funktor, der Applicativeaber keinMonad weil Gesetze nicht erfüllt werden können, obwohl die Typensignatur von bindimplementiert werden kann.

Dieses Beispiel hat einige Diskussionen ausgelöst, daher kann man mit Sicherheit sagen, dass es nicht einfach ist, dieses Beispiel als richtig zu beweisen. Mehrere Personen haben dies jedoch unabhängig voneinander mit unterschiedlichen Methoden überprüft. Siehe Ist `Daten PoE a = Leer | Paar aa` eine Monade? für zusätzliche Diskussion.

 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

Es ist etwas umständlich zu beweisen, dass es keine rechtmäßige MonadInstanz gibt. Der Grund für das nicht-monadische Verhalten ist, dass es keine natürliche Möglichkeit gibt, zu implementieren, bindwann eine Funktion zurückkehren f :: a -> B bkönnte Nothingoder Justfür unterschiedliche Werte von a.

Es ist vielleicht klarer zu überlegen Maybe (a, a, a), was auch keine Monade ist, und zu versuchen, dies umzusetzen join. Man wird feststellen, dass es keinen intuitiv vernünftigen Weg zur Implementierung gibt 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.

In den von angegebenen Fällen ???scheint es klar zu sein, dass wir Just (z1, z2, z3)aus sechs verschiedenen Typwerten keine vernünftige und symmetrische Weise erzeugen können a. Wir könnten sicherlich eine beliebige Teilmenge dieser sechs Werte wählen - zum Beispiel immer die erste MaybeNicht- Leere -, aber dies würde die Gesetze der Monade nicht erfüllen. Die Rücksendung Nothingwird auch nicht den Gesetzen entsprechen.

  • Eine baumartige Datenstruktur, die keine Monade ist , obwohl sie assoziativ ist bind- aber die Identitätsgesetze nicht erfüllt.

Die übliche baumartige Monade (oder "ein Baum mit funktorförmigen Zweigen") ist definiert als

 data Tr f a = Leaf a | Branch (f (Tr f a))

Dies ist eine kostenlose Monade über den Funktor f. Die Form der Daten ist ein Baum, in dem jeder Verzweigungspunkt ein "funktorreicher" Teilbaum ist. Der Standard-Binärbaum würde mit erhalten werden type f a = (a, a).

Wenn wir diese Datenstruktur modifizieren, indem wir auch die Blätter in der Form des Funktors herstellen f, erhalten wir das, was ich als "Semimonade" bezeichne - es binderfüllt die Natürlichkeits- und Assoziativitätsgesetze, aber seine pureMethode verfehlt eines der Identitätsgesetze. "Semimonaden sind Halbgruppen in der Kategorie der Endofunktoren. Was ist das Problem?" Dies ist die Typklasse Bind.

Der Einfachheit halber definiere ich die joinMethode anstelle von 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)

Die Asttransplantation ist Standard, aber die Blatttransplantation ist nicht Standard und erzeugt a Branch . Dies ist kein Problem für das Assoziativitätsgesetz, sondern verstößt gegen eines der Identitätsgesetze.

Wann haben Polynomtypen Monadeninstanzen?

Keiner der Funktoren Maybe (a, a)und Maybe (a, a, a)kann eine rechtmäßige MonadInstanz gegeben werden, obwohl sie offensichtlich sind Applicative.

Diese Funktoren haben keine Tricks - nein Voidoder bottomnirgendwo, keine knifflige Faulheit / Strenge, keine unendlichen Strukturen und keine Einschränkungen für Typklassen. Die ApplicativeInstanz ist völlig Standard. Die Funktionen returnund bindkönnen für diese Funktoren implementiert werden, erfüllen jedoch nicht die Gesetze der Monade. Mit anderen Worten, diese Funktoren sind keine Monaden, weil eine bestimmte Struktur fehlt (aber es ist nicht leicht zu verstehen, was genau fehlt). Zum Beispiel kann eine kleine Änderung im Funktor daraus eine Monade machen: data Maybe a = Nothing | Just aist eine Monade. Ein weiterer ähnlicher Funktordata P12 a = Either a (a, a) ist ebenfalls eine Monade.

Konstruktionen für Polynommonaden

Im Allgemeinen sind hier einige Konstruktionen aufgeführt, die Monadaus Polynomtypen rechtmäßige s erzeugen . In all diesen Konstruktionen Mist eine Monade:

  1. type M a = Either c (w, a) wo w ist irgendein Monoid?
  2. type M a = m (Either c (w, a))Wo mist eine Monade und wist ein Monoid
  3. type M a = (m1 a, m2 a)wo m1und m2sind irgendwelche Monaden
  4. type M a = Either a (m a)Wo mist eine Monade?

Die erste Konstruktion ist WriterT w (Either c), die zweite Konstruktion ist WriterT w (EitherT c m). Die dritte Konstruktion ist ein komponentenweise Produkt Monadengemeinschaft: pure @Mist definiert als das komponentenweise Produkt aus pure @m1und pure @m2und join @Mwird durch Weglassen Kreuzproduktdaten definiert (zB m1 (m1 a, m2 a)zugeordnet wird m1 (m1 a)durch den zweiten Teil des Tupels Weglassen):

 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))

Die vierte Konstruktion ist definiert als

 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

Ich habe überprüft, ob alle vier Konstruktionen rechtmäßige Monaden produzieren.

Ich vermute, dass es keine anderen Konstruktionen für Polynommonaden gibt. Zum Beispiel wird der Funktor Maybe (Either (a, a) (a, a, a, a))durch keine dieser Konstruktionen erhalten und ist daher nicht monadisch. Allerdings Either (a, a) (a, a, a)ist monadischen , weil es isomorph zum Produkt von drei Monaden ist a, aund Maybe a. Auch Either (a,a) (a,a,a,a)ist monadisch, weil es isomorph zum Produkt von aund ist Either a (a, a, a).

Die vier oben gezeigten Konstruktionen ermöglichen es uns, eine beliebige Summe einer beliebigen Anzahl von Produkten einer beliebigen Anzahl von abeispielsweise zu erhalten Either (Either (a, a) (a, a, a, a)) (a, a, a, a, a))und so weiter. Alle derartigen Typkonstruktoren haben (mindestens eine) MonadInstanz.

Es bleibt natürlich abzuwarten, welche Anwendungsfälle für solche Monaden existieren könnten. Ein weiteres Problem besteht darin, dass die Monadüber die Konstruktionen 1 bis 4 abgeleiteten Instanzen im Allgemeinen nicht eindeutig sind. Beispielsweise type F a = Either a (a, a)kann dem Typkonstruktor eine MonadInstanz auf zwei Arten zugewiesen werden: durch Konstruktion 4 unter Verwendung der Monade (a, a)und durch Konstruktion 3 unter Verwendung des Typisomorphismus Either a (a, a) = (a, Maybe a). Auch hier ist es nicht sofort offensichtlich, Anwendungsfälle für diese Implementierungen zu finden.

Es bleibt eine Frage - bei einem beliebigen Polynomdatentyp zu erkennen, ob eine MonadInstanz vorhanden ist. Ich weiß nicht, wie ich beweisen soll, dass es keine anderen Konstruktionen für Polynommonaden gibt. Ich glaube, es gibt bisher keine Theorie, um diese Frage zu beantworten.

winitzki
quelle
Ich denke B ist eine Monade. Können Sie dieser Bindung ein Gegenbeispiel geben Pair x y >>= f = case (f x, f y) of (Pair x' _,Pair _ y') -> Pair x' y' ; _ -> Empty?
Franky
@Franky Associativity schlägt mit dieser Definition fehl, wenn Sie eine fsolche auswählen , f xdie Emptyaber f yeine ist Pair, und im nächsten Schritt sind es beide Pair. Ich habe von Hand überprüft, dass die Gesetze für diese Implementierung oder für eine andere Implementierung nicht gelten. Aber es ist ein gutes Stück Arbeit, das zu tun. Ich wünschte, es gäbe einen einfacheren Weg, dies herauszufinden!
Winitzki
1
@Turion Dieses Argument gilt nicht für, Maybeda Maybees keine unterschiedlichen Werte enthält, über adie Sie sich Sorgen machen müssen.
Daniel Wagner
1
@Turion Ich habe dies durch ein paar Seiten Berechnungen bewiesen; Das Argument über "natürlichen Weg" ist nur eine heuristische Erklärung. Ein MonadBeispiel besteht aus Funktionen returnund binddaß erfüllen Gesetze. Es gibt zwei Implementierungen von returnund 25 Implementierungen bind, die den erforderlichen Typen entsprechen. Sie können durch direkte Berechnung zeigen, dass keine der Implementierungen den Gesetzen entspricht. Um den Arbeitsaufwand zu reduzieren, habe ich joinanstelle bindder Identitätsgesetze zuerst die Identitätsgesetze verwendet. Aber es war ein gutes Stück Arbeit.
Winitzki
1
@duplode Nein, ich glaube nicht, dass Traversablees nötig ist. m (Either a (m a))wird mit pure @min transformiert m (Either (m a) (m a)). Dann trivial Either (m a) (m a) -> m a, und wir können verwenden join @m. Das war die Implementierung, für die ich die Gesetze überprüft habe.
Winitzki