Pfadabhängige Typen in Haskell

Question

Ich versuche, eine API für einige Datenbanksysteme in Haskell zu entwerfen, und ich möchte die Spalten dieser Datenbank so modellieren, dass Interaktionen zwischen Spalten verschiedener Tabellen nicht durcheinander gebracht werden können.

Genauer gesagt, vorstellen, dass Sie eine Art eine Tabelle in einer Datenbank zu repräsentieren, zu irgendeiner Art verbunden:

type Table a = ... 

und dass Sie die Spalten der Tabelle entnehmen können, zusammen mit der Art der Spalte:

type Column col = ... 

Schließlich gibt es verschiedene Extraktoren. Zum Beispiel, wenn Ihre Tabelle Beschreibungen von Frösche enthält, würden wir eine Funktion extrahieren Sie die Spalte das Gewicht des Frosches enthält:

extractCol :: Table Frog -> Column Weight 

Hier ist die Frage: Ich möchte den Ursprung der Spalten unterscheiden, so dass Benutzer können keine Operationen zwischen Tabellen ausführen. Zum Beispiel:

bullfrogTable = undefined :: Table Frog 
toadTable = undefined :: Table Frog 
bullfrogWeights = extractCol bullfrogTable 
toadWeights = extractCol toadTable 
-- Or some other columns from the toad table 
toadWeights' = extractCol toadTable 
-- This should compile 
addWeights toadWeights' toadWeights 
-- This should trigger a type error 
addWeights bullfrogWeights toadWeights 

Ich weiß, wie dies in Scala zu erreichen (wegabhängige Typen finden Sie unter [1]), und ich habe in Haskell von 3 Optionen gedacht:

• nicht Verwenden von Typen und Ausführen einer Überprüfung zur Laufzeit (die aktuelle Lösung)

• Die TypeInType-Erweiterung, um einen Phantomtyp für den Tabellentyp selbst hinzuzufügen und diesen zusätzlichen Typ an die Spalten zu übergeben. Ich bin nicht scharf darauf, weil die Konstruktion eines solchen Typs sehr kompliziert wäre (Tabellen werden durch komplexe DAG-Operationen erzeugt) und wahrscheinlich in diesem Zusammenhang nur langsam kompiliert werden.

• Wrapping der Operationen mit einem forall Konstrukt ähnlich der ST Monade, aber in meinem Fall möchte ich die zusätzliche Tagging-Typ tatsächlich die Konstruktion zu entkommen.

Ich bin glücklich, ein sehr begrenzte Gültigkeit Scoping für den Bau von denselben Spalten zu haben (dh Spalten von table und (id table) nicht mischbare sind) und ich vor allem über das DSL-Gefühl des API kümmern, anstatt die Sicherheit.

[1] What is meant by Scala's path-dependent types?

Meine aktuelle Lösung

Hier ist, was ich tun endete, mit RankNTypes.

Ich möchte noch Benutzer die Möglichkeit geben, Spalten zu verwenden, wie sie für richtig halten, ohne einige starke Typprüfungen, und Opt-in, wenn sie einige stärkere Typgarantien wünschen: Dies ist ein DSL für Datenwissenschaftler, die die Macht nicht kennen die Haskell Seite

Tabellen sind immer noch von ihrem Inhalt des Stichwort:

type Table a = ... 

und Spalten werden nun mit einigen zusätzlichen Referenztypen, oben auf die Art der Daten, die sie enthalten getaggt:

type Column ref col = ... 

Projektionen von Tabellen zu Spalten sind entweder markiert oder unmarkiert. In der Praxis verbirgt sich dies hinter einem linsenartigen DSL.

extractCol :: Table Frog -> Column Frog Weight 

data TaggedTable ref a = TaggedTable { _ttTable :: Table a } 

extractColTagged :: Table ref Frog -> Column ref Weight 

withTag :: Table a -> (forall ref. TaggedTable ref a -> b) -> b 
withTag tb f = f (TaggedTable tb) 

Jetzt kann ich einige Code schreiben, wie folgend:

let doubleToadWeights = withTag toadTable $ \ttoadTable -> 
    let toadWeights = extractColTagged ttoadTable in 
    addWeights toadWeights toadWeights 

und dies wird nicht kompiliert, wie gewünscht:

let doubleToadWeights = 
    toadTable `withTag` \ttoads -> 
    bullfrogTable `withTag` \tbullfrogs -> 
     let toadWeights = extractColTagged ttoads 
      bullfrogWeights = extractColTagged tbullfrogs 
     in addWeights toadWeights bullfrogWeights -- Type error 

Von einem DSL-Perspektive, ich glaube, es ist nicht so so einfach wie das, was man mit Scala erreichen konnte, aber die Typfehlermeldung ist verständlich, was für mich von höchster Bedeutung ist.

Answer 1

Haskell hat (soweit ich weiß) keine pfadabhängigen Typen, aber Sie können einen Teil des Weges nutzen, indem Sie Rang 2-Typen verwenden. Zum Beispiel hat der ST Monade einen Dummy-Typ-Parameter s die Leckage zwischen Anrufungen von runST verwendet wird, zu verhindern:

runST :: (forall s . ST s a) -> a 

Innerhalb einer ST-Aktion können Sie eine STref haben:

newSTRef :: a -> ST s (STRef s a) 

Aber die STref Sie get trägt den s Typparameter, so dass es nicht erlaubt ist, aus dem runST zu entkommen.