Die kanonische 'Monad-Instanz' für die gemeinsame Nutzung der Umgebung plus Nichtdeterminismus ist wie folgt (mit Pseudo-Haskell, da Haskells Data.Set natürlich nicht monadisch ist):
Wenn man versucht, eine 'Container'-Monade wie Powerset (List, Writer, etc.) mit einer zweiten Monade m (hier, grob, Reader) zu kombinieren, wird' m 'um die Container-Monade gewickelt, wie oben beschrieben.
Ich frage mich dann nach der folgenden möglichen Powerset-over-Reader-Spezifikation:
%Vor% Das scheint nicht offensichtlich verrückt zu sein (ich weiß, dass GHCi rb r == rb' r für viele rb und rb' nicht überprüfen kann), aber bind' ist kompliziert genug, um es (für mich) schwierig zu machen überprüfe, ob die Monadengesetze gelten.
Meine Frage ist dann, ob eta' und bind' wirklich monadisch sind - und wenn nicht, welches der Gesetze wird verletzt und welcher Art von unerwartetem Verhalten könnte dies entsprechen?
Eine zweite Frage, die davon ausgeht, dass eta' und bind' nicht monadisch sind, ist, wie man feststellen kann, ob Funktionen mit diesen Typen gibt, die?
Spaßfrage. Hier ist meine Aufnahme - mal sehen, ob ich irgendwo nicht blöd gemacht habe!
Zunächst werde ich Ihre Signaturen in (etwas weniger pseudo) Haskell buchstabieren:
%Vor% Bevor wir fortfahren, sollten wir zwei praktische Komplikationen erwähnen. Erstens, wie Sie bereits festgestellt haben, ist es dank der Eq - und / oder Ord - Einschränkungen nicht trivial, die Mengen Functor oder Monad Instanzen zu vergeben; Auf jeden Fall gibt es Möglichkeiten, . Zweitens, und noch beunruhigender, mit dem Typ, den Sie für (>>=) vorschlagen, ist es notwendig, a s aus PSet (r -> a) zu extrahieren, ohne eine offensichtliche Versorgung von r s zu haben - oder, Mit anderen Worten, Ihre (>>=) erfordert eine Traversierung der Funktion funktor (->) r . Das ist natürlich im allgemeinen Fall nicht möglich und auch wenn möglich - zumindest was Haskell angeht - unpraktisch. In jedem Fall ist es für unsere spekulativen Zwecke in Ordnung, anzunehmen, dass wir (->) r durchlaufen können, indem wir die Funktion auf alle möglichen r -Werte anwenden. Ich werde dies durch ein hand-welliges universe :: PSet r set angeben, das zu Ehren dieses Pakets genannt wird . Ich werde auch eine universe :: PSet (r -> b) verwenden und annehmen, dass wir sagen können, ob zwei r -> b -Funktionen in einer bestimmten r übereinstimmen, auch ohne dass eine Eq -Restriktion erforderlich ist. (Der Pseudo-Haskell wird tatsächlich ziemlich falsch!)
Vorbemerkungen, hier sind meine Pseudo-Haskell-Versionen Ihrer Methoden:
%Vor%Als nächstes die Monadengesetze:
%Vor% (Übrigens, wenn man so etwas macht, ist es gut, die anderen Präsentationen der Klasse, mit der wir arbeiten, zu beachten - in diesem Fall haben wir join und (>=>) als Alternativen zu (>>=) - als Switching-Präsentationen könnte das Arbeiten mit Ihrer Instanz der Wahl angenehmer sein Hier bleibe ich bei der (>>=) Präsentation von Monad .)
Weiter zum ersten Gesetz ...
%Vor%Eins runter, zwei zu gehen.
%Vor% return y >>= f könnte daher möglicherweise eine viel größere Menge als f y sein. Wir haben eine Verletzung des zweiten Gesetzes; daher haben wir keine Monade - zumindest nicht mit der hier vorgeschlagenen Instanz.
Anhang: Hier ist eine aktuelle, lauffähige Implementierung Ihrer Funktionen, die zumindest für das Spielen mit kleinen Typen ausreichend ist. Es nutzt das bereits erwähnte Universum Paket.
%Vor%Es ist etwas einfacher, die Gesetze in der Kleisli-Notation zu überprüfen.
%Vor% Versuchen wir, return 'kleisli'' f = f zu verifizieren.
Sagen Sie alle unsere Typen a , b , c und r sind Integer und f x = {const x, const -x} . Welche Funktionen gibt es in (return 'kleisli'' f) 5 ? Dieser Satz sollte f 5 sein, also {const 5, const -5} .
Ist es? Natürlich sind const 5 und const -5 beide in, aber nicht nur. Zum Beispiel ist auch \r->if even r then 5 else -5 in.
Tags und Links haskell monads reader-monad