Ich möchte ein Wiki (eine Reihe von Dokumenten mit einem gerichteten Diagramm) in Dhall darstellen. Diese Dokumente werden in HTML gerendert, und ich möchte verhindern, dass jemals fehlerhafte Links generiert werden. Aus meiner Sicht könnte dies erreicht werden, indem entweder ungültige Diagramme (Diagramme mit Links zu nicht vorhandenen Knoten) durch das Typsystem nicht darstellbar gemacht werden oder indem eine Funktion geschrieben wird, um eine Liste von Fehlern in einem möglichen Diagramm zurückzugeben (z. B. "In möglichem Diagramm" X, Knoten A enthält einen Link zu einem nicht existierenden Knoten B ").
Eine naive Adjazenzlisten-Darstellung könnte ungefähr so aussehen:
let Node : Type = {
id: Text,
neighbors: List Text
}
let Graph : Type = List Node
let example : Graph = [
{ id = "a", neighbors = ["b"] }
]
in example
Wie dieses Beispiel zeigt, lässt dieser Typ Werte zu, die keinen gültigen Graphen entsprechen (es gibt keinen Knoten mit der ID "b", aber der Knoten mit der ID "a" legt einen Nachbarn mit der ID "b" fest). Darüber hinaus ist es nicht möglich, eine Liste dieser Probleme durch Umklappen der Nachbarn jedes Knotens zu erstellen, da Dhall den String-Vergleich nicht beabsichtigt.
Gibt es eine Darstellung, die entweder die Berechnung einer Liste defekter Links oder den Ausschluss defekter Links durch das Typsystem ermöglicht?
UPDATE: Ich habe gerade entdeckt, dass Naturals in Dhall vergleichbar sind. Ich nehme an, eine Funktion könnte geschrieben werden, um ungültige Kanten ("defekte Links") und doppelte Verwendungen eines Bezeichners zu identifizieren, wenn die Bezeichner Naturals wären.
Die ursprüngliche Frage, ob ein Graphentyp definiert werden kann, bleibt jedoch offen.
quelle
Antworten:
Ja, Sie können in Dhall einen typsicheren, gerichteten, möglicherweise zyklischen Graphen wie folgt modellieren:
Diese Darstellung garantiert das Fehlen von gebrochenen Kanten.
Ich habe diese Antwort auch in ein Paket umgewandelt, das Sie verwenden können:
Bearbeiten: Hier sind relevante Ressourcen und zusätzliche Erklärungen, die helfen können, die Vorgänge zu beleuchten:
Beginnen Sie zunächst mit dem folgenden Haskell-Typ für einen Baum :
Sie können sich diesen Typ als eine faule und möglicherweise unendliche Datenstruktur vorstellen, die darstellt, was Sie erhalten würden, wenn Sie nur weiterhin Nachbarn besuchen würden.
Nun lassen Sie uns so tun , dass die obige
Tree
Darstellung tatsächlich ist unsereGraph
nur durch Umbenennung der DatentypGraph
:... aber selbst wenn wir diesen Typ verwenden wollten, haben wir keine Möglichkeit, diesen Typ direkt in Dhall zu modellieren, da die Dhall-Sprache keine integrierte Unterstützung für rekursive Datenstrukturen bietet. Also, was machen wir?
Glücklicherweise gibt es tatsächlich eine Möglichkeit, rekursive Datenstrukturen und rekursive Funktionen in eine nicht rekursive Sprache wie Dhall einzubetten. Tatsächlich gibt es zwei Möglichkeiten!
Das erste, was ich las, das mich in diesen Trick einführte, war der folgende Entwurf eines Beitrags von Wadler:
... aber ich kann die Grundidee mit den folgenden zwei Haskell-Typen zusammenfassen:
... und:
Die Art
LFix
und Weise und dieGFix
Arbeit besteht darin, dass Sie ihnen "eine Ebene" Ihres gewünschten rekursiven oder "corecursiven" Typs (dh denf
) geben können, und sie geben Ihnen dann etwas, das so leistungsfähig ist wie der gewünschte Typ, ohne dass Sprachunterstützung für Rekursion oder Corecursion erforderlich ist .Verwenden wir Listen als Beispiel. Wir können "eine Ebene" einer Liste mit dem folgenden
ListF
Typ modellieren :Vergleichen Sie diese Definition mit der Definition
OrdinaryList
einer gewöhnlichen rekursiven Datentypdefinition:Der Hauptunterschied besteht darin, dass
ListF
ein zusätzlicher Typparameter (next
) verwendet wird, den wir als Platzhalter für alle rekursiven / corecursiven Vorkommen des Typs verwenden.Ausgestattet mit
ListF
können wir nun rekursive und kursive Listen wie folgt definieren:... wo:
List
ist eine rekursive Liste, die ohne Sprachunterstützung für die Rekursion implementiert istCoList
ist eine CoreCursive-Liste, die ohne Sprachunterstützung für Corecursion implementiert wurdeBeide Typen sind äquivalent zu ("isomorph zu")
[]
, was bedeutet, dass:List
und reversibel hin und her konvertieren[]
CoList
und reversibel hin und her konvertieren[]
Lassen Sie uns das beweisen, indem wir diese Konvertierungsfunktionen definieren!
Der erste Schritt bei der Implementierung des Dhall-Typs bestand also darin, den rekursiven
Graph
Typ zu konvertieren :... zur äquivalenten co-rekursiven Darstellung:
... obwohl ich es zur Vereinfachung der Typen ein wenig einfacher finde, mich
GFix
auf den Fall zu spezialisieren, in demf = GraphF
:Haskell hat keine anonymen Datensätze wie Dhall, aber wenn dies der Fall wäre, könnten wir den Typ weiter vereinfachen, indem wir die Definition von
GraphF
:Jetzt fängt dies an, wie der Dhall-Typ für a auszusehen
Graph
, besonders wenn wir ersetzenx
durchnode
:Es gibt jedoch noch einen letzten kniffligen Teil, nämlich die Übersetzung
ExistentialQuantification
von Haskell nach Dhall. Es stellt sich heraus, dass Sie existenzielle Quantifizierung immer in universelle Quantifizierung (dhforall
) unter Verwendung der folgenden Äquivalenz übersetzen können:Ich glaube, das nennt man "Skolemisierung"
Weitere Einzelheiten finden Sie unter:
... und dieser letzte Trick gibt Ihnen den Dhall-Typ:
... wobei
forall (Graph : Type)
die gleiche Rolle wieforall x
in der vorherigen Formel undforall (Node : Type)
die gleiche Rolle wieforall y
in der vorherigen Formel spielt.quelle