wake-up-neo.com

Was ist eine indizierte Monade?

Was ist indizierte Monade und die Motivation für diese Monade?

Ich habe gelesen, dass es hilft, die Nebenwirkungen im Auge zu behalten. Aber die Typensignatur und Dokumentation führen mich nirgendwo hin.

Was wäre ein Beispiel dafür, wie es helfen kann, die Nebenwirkungen im Auge zu behalten (oder ein anderes gültiges Beispiel)?

94
Sibi

Wie immer ist die Terminologie, die die Menschen verwenden, nicht ganz konsistent. Es gibt eine Vielzahl von Monaden-inspiriert-aber-streng genommen-nicht-ganz-Vorstellungen. Der Begriff "indizierte Monade" ist eine Zahl (einschließlich "Monade" und "parametrisierte Monade" (für sie der Name von Atkey)) von Begriffen, die zur Charakterisierung eines solchen Begriffs verwendet werden. (Wenn Sie daran interessiert sind, ist ein weiterer solcher Begriff Katsumatas "parametrische Effektmonade", die durch ein Monoid indiziert wird, wobei die Rendite neutral indiziert wird und die Bindung im Index akkumuliert.)

Lassen Sie uns zunächst die Arten prüfen.

IxMonad (m :: state -> state -> * -> *)

Das heißt, die Art einer "Berechnung" (oder "Aktion", wenn Sie es vorziehen, aber ich bleibe bei "Berechnung") sieht aus wie

m before after value

wo before, after :: state und value :: *. Die Idee ist es, die Mittel zu erfassen, um sicher mit einem externen System zu interagieren, das eine vorhersehbare Zustandsvorstellung hat. Der Typ einer Berechnung gibt an, wie der Status lauten muss before, wie der Status lauten soll after und (wie bei regulären Monaden über *) welche Art von value erzeugt die Berechnung.

Die üblichen Kleinigkeiten sind *- wie eine Monade und state - wie ein Domino.

ireturn  ::  a -> m i i a    -- returning a pure value preserves state
ibind    ::  m i j a ->      -- we can go from i to j and get an a, thence
             (a -> m j k b)  -- we can go from j to k and get a b, therefore
             -> m i k b      -- we can indeed go from i to k and get a b

Der so erzeugte Begriff "Kleisli-Pfeil" (Funktion, die eine Berechnung ergibt) ist

a -> m i j b   -- values a in, b out; state transition i to j

und wir bekommen eine Komposition

icomp :: IxMonad m => (b -> m j k c) -> (a -> m i j b) -> a -> m i k c
icomp f g = \ a -> ibind (g a) f

und wie immer stellen die Gesetze genau sicher, dass ireturn und icomp uns eine Kategorie geben

      ireturn `icomp` g = g
      f `icomp` ireturn = f
(f `icomp` g) `icomp` h = f `icomp` (g `icomp` h)

oder, in Comedy Fake C/Java/was auch immer,

      g(); skip = g()
      skip; f() = f()
{g(); h()}; f() = h(); {g(); f()}

Warum die Mühe? "Regeln" der Interaktion modellieren. Beispielsweise können Sie eine DVD nicht auswerfen, wenn sich keine im Laufwerk befindet, und Sie können keine DVD in das Laufwerk legen, wenn sich bereits eine darin befindet. So

data DVDDrive :: Bool -> Bool -> * -> * where  -- Bool is "drive full?"
  DReturn :: a -> DVDDrive i i a
  DInsert :: DVD ->                   -- you have a DVD
             DVDDrive True k a ->     -- you know how to continue full
             DVDDrive False k a       -- so you can insert from empty
  DEject  :: (DVD ->                  -- once you receive a DVD
              DVDDrive False k a) ->  -- you know how to continue empty
             DVDDrive True k a        -- so you can eject when full

instance IxMonad DVDDrive where  -- put these methods where they need to go
  ireturn = DReturn              -- so this goes somewhere else
  ibind (DReturn a)     k  = k a
  ibind (DInsert dvd j) k  = DInsert dvd (ibind j k)
  ibind (DEject j)      k  = DEject j $ \ dvd -> ibind (j dvd) k

Damit können wir die "primitiven" Befehle definieren

dInsert :: DVD -> DVDDrive False True ()
dInsert dvd = DInsert dvd $ DReturn ()

dEject :: DVDrive True False DVD
dEject = DEject $ \ dvd -> DReturn dvd

aus denen andere mit ireturn und ibind zusammengesetzt werden. Jetzt kann ich schreiben (Ausleihe do - Notation)

discSwap :: DVD -> DVDDrive True True DVD
discSwap dvd = do dvd' <- dEject; dInsert dvd ; ireturn dvd'

aber nicht das physikalisch Unmögliche

discSwap :: DVD -> DVDDrive True True DVD
discSwap dvd = do dInsert dvd; dEject      -- ouch!

Alternativ kann man seine primitiven Befehle direkt definieren

data DVDCommand :: Bool -> Bool -> * -> * where
  InsertC  :: DVD -> DVDCommand False True ()
  EjectC   :: DVDCommand True False DVD

und instanziieren Sie dann die generische Vorlage

data CommandIxMonad :: (state -> state -> * -> *) ->
                        state -> state -> * -> * where
  CReturn  :: a -> CommandIxMonad c i i a
  (:?)     :: c i j a -> (a -> CommandIxMonad c j k b) ->
                CommandIxMonad c i k b

instance IxMonad (CommandIxMonad c) where
  ireturn = CReturn
  ibind (CReturn a) k  = k a
  ibind (c :? j)    k  = c :? \ a -> ibind (j a) k

Tatsächlich haben wir gesagt, was die primitiven Kleisli-Pfeile sind (was ein "Domino" ist), und dann einen geeigneten Begriff der "Berechnungssequenz" über sie gebaut.

Beachten Sie, dass für jede indizierte Monade m die "no change diagonal" m i i ist eine Monade, aber im Allgemeinen m i j ist nicht. Darüber hinaus werden Werte nicht indiziert, sondern Berechnungen werden indiziert, sodass eine indizierte Monade nicht nur die übliche Idee einer Monade ist, die für eine andere Kategorie instanziiert wurde.

Schauen Sie sich noch einmal die Art eines Kleisli-Pfeils an

a -> m i j b

Wir wissen, dass wir uns im Status i befinden müssen, um zu starten, und wir gehen davon aus, dass jede Fortsetzung im Status j beginnt. Wir wissen viel über dieses System! Dies ist keine riskante Operation! Wenn wir die DVD ins Laufwerk legen, geht es rein! Das DVD-Laufwerk bekommt nach jedem Befehl keine Aussage über den Status.

Aber im Allgemeinen stimmt das nicht, wenn man mit der Welt interagiert. Manchmal muss man vielleicht etwas Kontrolle abgeben und die Welt tun lassen, was sie will. Wenn Sie beispielsweise ein Server sind, können Sie Ihrem Client eine Auswahlmöglichkeit anbieten, und Ihr Sitzungsstatus hängt von der Auswahl ab. Die "Angebotsauswahl" -Operation des Servers bestimmt nicht den resultierenden Status, aber der Server sollte trotzdem weitermachen können. Es ist kein "primitiver Befehl" im obigen Sinne, daher sind indizierte Monaden kein so gutes Werkzeug, um das nvorhersehbare -Szenario zu modellieren.

Was ist ein besseres Werkzeug?

type f :-> g = forall state. f state -> g state

class MonadIx (m :: (state -> *) -> (state -> *)) where
  returnIx    :: x :-> m x
  flipBindIx  :: (a :-> m b) -> (m a :-> m b)  -- tidier than bindIx

Gruselige Kekse? Nicht wirklich, aus zwei Gründen. Erstens sieht es eher so aus, als wäre es eine Monade, weil es ist eine Monade ist, aber über (state -> *) eher, als *. Zweitens, wenn Sie sich die Art eines Kleisli-Pfeils ansehen,

a :-> m b   =   forall state. a state -> m b state

sie erhalten die Art der Berechnungen mit Vorbedingunga und Nachbedingung b, genau wie in Good Old Hoare Logic. Behauptungen in der Programmlogik haben weniger als ein halbes Jahrhundert gedauert, um die Curry-Howard-Korrespondenz zu durchqueren und zu Haskell-Typen zu werden. Der Typ returnIx besagt "Sie können jede Nachbedingung erreichen, die gilt, indem Sie einfach nichts tun", was die Hoare-Logik-Regel für "Überspringen" ist. Die entsprechende Komposition ist die Hoare-Logik-Regel für ";".

Lassen Sie uns zum Schluss den Typ von bindIx betrachten und alle Quantifizierer eingeben.

bindIx :: forall i. m a i -> (forall j. a j -> m b j) -> m b i

Diese forall haben eine entgegengesetzte Polarität. Wir wählen den Anfangszustand i und eine Berechnung, die bei i mit der Nachbedingung a beginnen kann. Die Welt wählt jeden Zwischenzustand j, den sie mag, aber sie muss uns den Beweis liefern, dass die Nachbedingung b gilt, und aus jedem solchen Zustand können wir b machen. halt. Wir können also nacheinander die Bedingung b aus dem Zustand i erreichen. Indem wir die Nach-Zustände loslassen, können wir nvorhersehbare Berechnungen modellieren.

Sowohl IxMonad als auch MonadIx sind nützlich. Beide Modelle sind gültig für interaktive Berechnungen in Bezug auf den sich ändernden Zustand, vorhersehbar bzw. unvorhersehbar. Vorhersehbarkeit ist wertvoll, wenn Sie sie erhalten können, aber Unvorhersehbarkeit ist manchmal eine Tatsache des Lebens. Hoffentlich gibt diese Antwort einen Hinweis darauf, was indizierte Monaden sind, und sagt voraus, wann sie nützlich werden und wann sie aufhören.

119
pigworker

Es gibt mindestens drei Möglichkeiten, eine indizierte Monade zu definieren, die ich kenne.

Ich werde diese Optionen als indizierte Monaden à la X bezeichnen, wobei X über den Informatikern Bob Atkey, Conor McBride und Dominic Orchard liegt So neige ich dazu, an sie zu denken. Teile dieser Konstruktionen haben durch die Kategorietheorie eine viel längere illustrere Geschichte und schönere Interpretationen, aber ich habe zuerst von ihnen erfahren, die mit diesen Namen verbunden sind, und ich versuche, diese Antwort davon abzuhalten, zu erhalten esoterisch.

Atkey

Bob Atkeys Stil der indizierten Monade besteht darin, mit zwei zusätzlichen Parametern zu arbeiten, um den Index der Monade zu verarbeiten.

Damit erhalten Sie die Definitionen, die die Leute in anderen Antworten herumgeworfen haben:

class IMonad m where
  ireturn  ::  a -> m i i a
  ibind    ::  m i j a -> (a -> m j k b) -> m i k b

Wir können auch indizierte Comonaden à la Atkey definieren. Ich bekomme tatsächlich eine Menge Kilometer aus diesen heraus in der lens Codebasis .

McBride

Die nächste Form der indizierten Monade ist die Definition von Conor McBride aus seiner Arbeit "Kleisli Arrows of Outrageous Fortune" . Er verwendet stattdessen einen einzelnen Parameter für den Index. Dadurch hat die indizierte Monadendefinition eine ziemlich clevere Form.

Wenn wir eine natürliche Transformation unter Verwendung der Parametrizität wie folgt definieren

type a ~> b = forall i. a i -> b i 

dann können wir McBrides Definition als aufschreiben

class IMonad m where
  ireturn :: a ~> m a
  ibind :: (a ~> m b) -> (m a ~> m b)

Das fühlt sich ganz anders an als bei Atkey, aber es fühlt sich eher wie eine normale Monade an, anstatt eine Monade auf (m :: * -> *), wir bauen es auf (m :: (k -> *) -> (k -> *).

Interessanterweise können Sie tatsächlich Atkeys Stil der indizierten Monade von McBride wiederherstellen, indem Sie einen cleveren Datentyp verwenden, den McBride in seinem unnachahmlichen Stil als "at key" bezeichnet.

data (:=) :: a i j where
   V :: a -> (a := i) i

Jetzt können Sie das herausfinden

ireturn :: IMonad m => (a := j) ~> m (a := j)

das erweitert sich zu

ireturn :: IMonad m => (a := j) i -> m (a := j) i

kann nur aufgerufen werden, wenn j = i, und wenn Sie dann ibind sorgfältig lesen, erhalten Sie dasselbe Ergebnis wie bei Atkey ibind. Sie müssen diese (: =) Datenstrukturen umgehen, aber sie stellen die Leistung der Atkey-Präsentation wieder her.

Andererseits ist die Atkey-Präsentation nicht stark genug, um alle Verwendungen der McBride-Version wiederherzustellen. Macht wurde strikt gewonnen.

Eine andere nette Sache ist, dass McBrides indizierte Monade eindeutig eine Monade ist, es ist nur eine Monade in einer anderen Funktorkategorie. Es funktioniert über Endofunktoren in der Kategorie der Funktoren von (k -> *) bis (k -> *) statt der Kategorie der Funktoren von * bis *.

Eine unterhaltsame Übung besteht darin, herauszufinden, wie die Konvertierung von McBride in Atkey für indizierte Comonaden durchgeführt wird. Ich persönlich verwende den Datentyp "At" für die "at key" -Konstruktion in McBrides Papier. Tatsächlich ging ich auf der ICFP 2013 zu Bob Atkey und erwähnte, dass ich ihn auf den Kopf gestellt hatte, um ihn in einen "Mantel" zu verwandeln. Er wirkte sichtlich verstört. Die Linie spielte sich in meinem Kopf besser ab. =)

Obstgarten

Schließlich ist ein dritter, weitaus weniger häufig genannter Antragsteller auf den Namen "indizierte Monade" auf Dominic Orchard zurückzuführen, der stattdessen ein Monoid auf Typebene verwendet, um Indizes zusammenzufassen. Anstatt die Details der Konstruktion durchzugehen, verlinke ich einfach zu diesem Vortrag:

http://www.cl.cam.ac.uk/~dao29/ixmonad/ixmonad-fita14.pdf

45
Edward KMETT

Nehmen Sie als einfaches Szenario an, Sie hätten eine staatliche Monade. Der Zustandstyp ist komplex groß, doch alle diese Zustände können in zwei Mengen unterteilt werden: rote und blaue Zustände. Einige Operationen in dieser Monade sind nur dann sinnvoll, wenn der aktuelle Status ein blauer Status ist. Unter diesen behalten einige den Zustand blau (blueToBlue), während andere den Zustand rot (blueToRed) machen. In einer regulären Monade könnten wir schreiben

blueToRed  :: State S ()
blueToBlue :: State S ()

foo :: State S ()
foo = do blueToRed
         blueToBlue

auslösen eines Laufzeitfehlers, da die zweite Aktion einen blauen Zustand erwartet. Dies möchten wir statisch verhindern. Indizierte Monade erfüllt dieses Ziel:

data Red
data Blue

-- assume a new indexed State monad
blueToRed  :: State S Blue Red  ()
blueToBlue :: State S Blue Blue ()

foo :: State S ?? ?? ()
foo = blueToRed `ibind` \_ ->
      blueToBlue          -- type error

Ein Typfehler wird ausgelöst, weil sich der zweite Index von blueToRed (Red) vom ersten Index von blueToBlue (Blue) unterscheidet.

Als ein weiteres Beispiel können Sie mit indizierten Monaden einer Zustandsmonade erlauben, den Typ für ihren Zustand zu ändern, z. du könntest haben

data State old new a = State (old -> (new, a))

Sie können den obigen Code verwenden, um einen Status zu erstellen, der ein statisch typisierter heterogener Stapel ist. Operationen hätten Typ

Push :: a -> State old (a,old) ()
pop  :: State (a,new) new a

Angenommen, Sie möchten eine eingeschränkte IO Monade, die keinen Dateizugriff zulässt. Sie könnten z.

openFile :: IO any FilesAccessed ()
newIORef :: a -> IO any any (IORef a)
-- no operation of type :: IO any NoAccess _

Auf diese Weise ist eine Aktion vom Typ IO ... NoAccess () statisch garantiert dateizugriffsfrei. Stattdessen kann eine Aktion vom Typ IO ... FilesAccessed () auf Dateien zugreifen. Eine indizierte Monade würde bedeuten, dass Sie keinen separaten Typ für die eingeschränkte E/A erstellen müssen, sodass jede nicht dateibezogene Funktion in beiden IO -Typen dupliziert werden muss.

23
chi

Eine indizierte Monade ist keine spezifische Monade wie beispielsweise die Staatsmonade, sondern eine Art Verallgemeinerung des Monadenkonzepts mit zusätzlichen Typparametern.

Während ein "Standard" -Monadenwert den Typ Monad m => m a Hat, ist ein Wert in einer indizierten Monade IndexedMonad m => m i j a, Wobei i und j Indextypen sind, sodass i ist der Indextyp am Anfang der monadischen Berechnung und j am Ende der Berechnung. In gewisser Weise können Sie sich i als eine Art Eingabetyp und j als Ausgabetyp vorstellen.

Am Beispiel von State behält eine zustandsbehaftete Berechnung State s a Während der gesamten Berechnung einen Zustand vom Typ s bei und gibt ein Ergebnis vom Typ a zurück. Eine indizierte Version, IndexedState i j a, Ist eine zustandsbezogene Berechnung, bei der sich der Zustand während der Berechnung in einen anderen Typ ändern kann. Der Anfangszustand hat den Typ i und der Zustand und das Ende der Berechnung den Typ j.

Die Verwendung einer indizierten Monade gegenüber einer normalen Monade ist selten erforderlich, kann jedoch in einigen Fällen zur Codierung strengerer statischer Garantien verwendet werden.

17
shang

Es kann wichtig sein, einen Blick darauf zu werfen, wie die Indizierung in abhängigen Typen verwendet wird (z. B. in agda). Dies kann erklären, wie die Indizierung im Allgemeinen hilft, und diese Erfahrung dann auf Monaden übertragen.

Indizierung ermöglicht das Herstellen von Beziehungen zwischen bestimmten Instanzen von Typen. Dann können Sie über einige Werte nachdenken, um festzustellen, ob diese Beziehung besteht.

Zum Beispiel können Sie (in agda) angeben, dass einige natürliche Zahlen mit _<_ Zusammenhängen, und der Typ gibt an, um welche Zahlen es sich handelt. Dann können Sie verlangen, dass einer Funktion ein Zeuge gegeben wird, der m < n Ist, weil nur dann die Funktion korrekt funktioniert - und ohne diesen Zeuge wird das Programm nicht kompiliert.

Als weiteres Beispiel könnten Sie bei ausreichender Ausdauer und Compilerunterstützung für die von Ihnen gewählte Sprache kodieren, dass die Funktion davon ausgeht, dass eine bestimmte Liste sortiert ist.

Indizierte Monaden erlauben es, einige der abhängigen Typsysteme zu codieren, um Nebenwirkungen genauer zu verwalten.

5
Sassa NF