Ich versuche in Haskell diesen Teil des Idris-Codes zu replizieren, der die korrekte Reihenfolge der Aktionen durch Typen erzwingt:
%Vor% Dank Überladen von (>>=) operator kann man einen monadischen Code schreiben wie:
, aber der Compiler weist falsche Übergänge wie:
zurück %Vor%Ich habe versucht, diesem Muster im folgenden Haskell-Fragment zu folgen:
%Vor% Aber das scheitert natürlich: Die Instanzen Applicative und Monad können nicht korrekt definiert werden, da sie zwei verschiedene Instanzen benötigen, um Operationen korrekt zu sequenzieren. Der Konstruktor Bind kann verwendet werden, um eine korrekte Sequenzierung zu erzwingen, aber ich kann es nicht schaffen, die "schönere" Do-Notation zu verwenden.
Wie könnte ich diesen Code schreiben, um die Do-Notation verwenden zu können, z. um ungültige Sequenzen von Command s zu verhindern?
Was Sie suchen, ist in der Tat Atkeys parametrisierte Monade , die jetzt bekannter ist als indizierte Monade .
%Vor% IMonad ist die Klasse der monadähnlichen Dinge m :: k -> k -> * -> * , die Pfade durch ein gerichtetes Diagramm von Typen beschreiben, die zum Typ k gehören. >>>= bindet eine Berechnung, die den Typstufenstatus von i nach j in eine Berechnung nimmt, die von j nach k geht und eine größere Berechnung von i nach k zurückgibt. Mit ireturn können Sie einen reinen Wert in eine monadische Berechnung aufheben, die den Status auf Typpegel nicht ändert.
Ich werde die indizierte freie Monade verwenden, um die Struktur dieser Art von Anfrage-Antwort-Aktion zu erfassen, hauptsächlich, weil ich nicht herausfinden möchte, wie ich den IMonad Instanz für Ihren Typ selbst:
Wir können Ihre Door monad kostenlos aus dem folgenden Funktor erstellen:
Sie können open eine Tür, wodurch eine momentan geschlossene Tür geöffnet wird, close eine momentan geöffnete Tür, oder ring die Glocke einer Tür, die geschlossen bleibt, vermutlich weil der Bewohner des Hauses dies nicht tut Ich will dich nicht sehen.
Schließlich bedeutet die Erweiterung RebindableSyntax , dass wir die Standardklasse Monad durch unsere eigene benutzerdefinierte IMonad ersetzen können.
Allerdings merke ich, dass du nicht wirklich die Bindungsstruktur deiner Monade verwendest. Keiner Ihrer Bausteine Open , Close oder Ring gibt einen Wert zurück. Also ich denke, was Sie wirklich brauchen, ist die folgende, einfachere Typ-ausgerichtete Liste Typ:
In der Praxis ist Path :: (k -> k -> *) -> k -> k -> * wie eine verkettete Liste, hat aber eine zusätzliche Struktur auf Typenebene, die wiederum einen Pfad durch ein gerichtetes Diagramm beschreibt, dessen Knoten sich in k befinden. Die Elemente der Liste sind Kanten g . Nil sagt, dass Sie immer einen Pfad von einem Knoten i zu sich selbst finden können und Cons erinnert uns daran, dass eine Reise von tausend Meilen mit einem einzigen Schritt beginnt: wenn Sie eine Kante von i bis j haben und einen Pfad von j bis k , können Sie diese kombinieren, um einen Pfad von i nach k zu erstellen. Es heißt eine typenausgerichtete Liste , da der Endtyp eines Elements mit dem Starttyp des nächsten Elements übereinstimmen muss.
Auf der anderen Seite von Curry-Howard Street, wenn g eine binäre logische Relation ist, konstruiert Path g seine reflexive transitive closure . Oder, kategorisch Path g ist der Typ von Morphismen in der freien Kategorie eines Graphen g . Das Verfassen von Morphismen in der freien Kategorie wird nur (umgedreht) zum Anhängen von typgerechten Listen.
Dann können wir Door in Path schreiben:
Sie erhalten do notation nicht (obwohl ich denke, RebindableSyntax erlaubt Ihnen, Listenliterale zu überladen), aber das Erstellen von Berechnungen mit (.) sieht aus wie die Sequenzierung von reinen Funktionen, die Ich denke, ist eine ziemlich gute Analogie für das, was Sie ohnehin tun. Für mich benötigt man zusätzliche Intelligenz - eine seltene und kostbare natürliche Ressource - um indizierte Monaden zu verwenden. Es ist besser, die Komplexität von Monaden zu vermeiden, wenn eine einfachere Struktur ausreicht.