Statisch sichere dynamische Eingabe à la Python

Hallo Habr.

Neulich entstand in einem meiner Hobbyprojekte die Aufgabe, ein Repository mit Metriken zu schreiben.

Die Aufgabe selbst ist sehr einfach gelöst, aber mein Problem mit dem Haskell (insbesondere bei Projekten zu meiner eigenen Unterhaltung) ist, dass es unmöglich ist, das Problem einfach anzunehmen und zu lösen. Es ist notwendig zu entscheiden, zu erweitern, zu abstrahieren, zu abstrahieren und dann weiter zu erweitern. Daher wollte ich die Speicherung von Metriken erweiterbar machen, um nicht im Voraus anzugeben, welche dort vorhanden sein würden. Dies an sich ist ein Thema für einen separaten Artikel, und heute werden wir eine kleine Zutat betrachten: das Schreiben eines typsicheren Wrappers für bisher unbekannte Typen. So etwas wie dynamisches Tippen, aber mit statischen Garantien, dass wir keinen Unsinn machen.

Ich denke, der Artikel wird erfahrenen Haskellisten nichts Neues eröffnen, aber jetzt werden wir zumindest diese Zutat aus der Verpackung nehmen und uns in den folgenden Artikeln nicht davon ablenken lassen. Naja, oder du kannst nicht so bescheiden sein und sagen, dass ich mir schon ein ganzes Designmuster ausgedacht habe.

Also formulieren wir zuerst das Problem. Wir müssen in der Lage sein, einige Objekte mit Werten bisher unbekannter Typen zu verknüpfen. Mit anderen Worten, es ist erforderlich, dass die Werte zuvor unbekannter Typen als Schlüssel in einer Art Karte fungieren.

Natürlich sind wir nicht verrückt und wir werden keine Unterstützung von Werten jeglicher Art benötigen. Wir fordern, dass der Typ (auch wenn er unbekannt ist) den Vergleich im Sinne der Bestellung unterstützt. In Haskell bedeutet dies, dass wir Typen a , die die Ord a Klasse implementieren.

Beachten Sie, dass wir Unterstützung für die Erstellung eines Hashs und die Überprüfung der Gleichheit verlangen könnten, aber aus einer Reihe von Gründen wäre es bequemer und klarer, uns auf den Vergleich zu beschränken.

Wenn es darum geht, Werte zu speichern, von denen bekannt ist, dass sie einen Klassentyp implementieren, werden in Haskell normalerweise existenzielle Typen verwendet:

 data SomeOrd where MkSomeOrd :: Ord a => a -> SomeOrd 

Wenn wir also ein Objekt vom Typ SomeOrd und dafür einen Mustervergleich durchgeführt haben:

 foo :: SomeOrd -> Bar foo (MkSomeOrd val) = ... (1) ... 

Dann wissen wir unter Punkt (1) nicht, welchen Typ val hat, aber wir wissen (und vor allem der Timer weiß auch), dass val die Ord Zeitklasse implementiert.

Wenn die Typfunktionen der Klasse jedoch zwei (oder mehr) Argumente implizieren, ist die Verwendung eines solchen Datensatzes von geringem Nutzen:

 tryCompare :: SomeOrd -> SomeOrd -> Bool tryCompare (MkSomeOrd val1) (MkSomeOrd val2) = ? 

Um die Ord Methoden verwenden zu können, müssen val und val2 gleichen Typ sein, dies muss jedoch überhaupt nicht erfolgen! Es stellt sich heraus, dass unser SomeOrd nutzlos ist. Was tun?

Trotz der Tatsache, dass Haskell eine kompilierte Sprache mit aggressiver Typlöschung ist (nach der Kompilierung sind sie im Allgemeinen nicht vorhanden), kann der Compiler auf Anfrage immer noch Vertreter von Laufzeittypen generieren. Die für Typ a repräsentative Rolle ist der Wert von Typ TypeRep a und Anfrage Die Generierung wird von Typeable Typeclass beantwortet.

Wenn wir außerdem zwei verschiedene Instanzen von rep1 :: TypeRep a, rep2 :: TypeRep b , können wir sie vergleichen und prüfen, ob sie denselben Typ darstellen oder nicht. Wenn sie tatsächlich denselben Typ darstellen, stimmt b offensichtlich mit b überein. Und vor allem liefert die Funktion der Überprüfung von Typdarstellungen auf Gleichheit ein Ergebnis, das den Typcher davon überzeugen kann:

 eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~~: b) 

Welcher Unsinn steht hier geschrieben?

Erstens ist eqTypeRep eine Funktion.

Zweitens ist es polymorph, aber nicht nur nach Typ, sondern auch nach Sorten dieser Typen. Dies wird durch den Teil für alle forall k1 k2 (a :: k1) (b :: k2) angezeigt - dies bedeutet, dass a und b nicht nur gewöhnliche Typen wie Int oder [String] , sondern auch beispielsweise berüchtigte Konstruktoren (siehe DataKinds und andere Versuche, Haskell zertifizieren zu lassen). Aber das alles brauchen wir nicht.

Drittens werden zwei Laufzeitdarstellungen potenziell unterschiedlicher Typen akzeptiert, TypeRep a und TypeRep b .

Viertens wird ein Wert vom Typ Maybe (a :~~: b) . Das Interessanteste passiert hier.

Wenn die Typen nicht übereinstimmen, gibt die Funktion das übliche Nothing und alles ist in Ordnung. Wenn die Typen übereinstimmen, gibt die Funktion Just val , wobei val vom Typ a :~~: b . Mal sehen, um welchen Typ es sich handelt:

 -- | Kind heterogeneous propositional equality. Like ':~:', @a :~~: b@ is -- inhabited by a terminating value if and only if @a@ is the same type as @b@. -- -- @since 4.10.0.0 data (a :: k1) :~~: (b :: k2) where HRefl :: a :~~: a 

Jetzt lass uns reden. Angenommen, wir erhalten einen Wert vom Typ a :~~: b . Wie könnte es gebaut werden? Der einzige Weg ist mit dem HRefl Konstruktor, und dieser Konstruktor erfordert, dass auf beiden Seiten des Symbols :~~: es dasselbe sein sollte. Daher fällt a mit b . Darüber hinaus, wenn wir zapternnom-match auf val , dann wird der taypcheker auch darüber wissen. Daher gibt die Funktion eqTypeRep Beweis zurück, dass zwei potenziell unterschiedliche Typen gleich sind, wenn sie tatsächlich gleich sind.

Im obigen Absatz habe ich jedoch gelogen. Niemand hält uns davon ab, so etwas in Haskell zu schreiben

 wrong :: Int :~~: String wrong = wrong --    

oder

 wrong :: Int :~~: String wrong = undefined 

oder brechen Sie das System mit einer Reihe von etwas weniger offensichtlichen Möglichkeiten. Dies ist eine der Manifestationen der in engen Kreisen bekannten, dass das Haskell als Logik inkonsistent ist. In Sprachen mit stärkeren Typsystemen werden solche Definitionen nicht gestempelt.

Aus diesem Grund wird in der oben zitierten Dokumentation der Endwert erwähnt. Beide Varianten der Implementierung von wrong oben erzeugen nicht diesen sehr terminierenden Wert, was uns ein wenig Grund und Vertrauen gibt: Wenn unser Programm auf dem Haskell beendet wurde (und nicht undefined ), entspricht sein Ergebnis den geschriebenen Typen. Hier gibt es jedoch einige Details im Zusammenhang mit Faulheit, aber wir werden dieses Thema nicht öffnen.

eqTypeRep ist die zweite Manifestation der Haskell-Schwäche im obigen Code der Typ der eqTypeRep Funktion. In stärkeren Sprachen würde es einen Wert eines stärkeren Typs zurückgeben, der nicht nur die Gleichheit der Typen beweisen würde, wenn sie tatsächlich gleich sind, sondern auch ihre Ungleichheit beweisen würde, wenn sie tatsächlich ungleich sind. Die Inkonsistenz der Haskell-Logik macht solche Funktionen jedoch ein wenig sinnlos: Es ist alles wichtig, wenn Sie die Sprache als Beweis für Theoreme und nicht als Programmiersprache verwenden und Haskell nicht als Beweis verwenden.

Na ja, genug von der Log- und Typentheorie, lassen Sie uns zu unseren Metriken zurückkehren. Jetzt zeichne einfach eine Eule Die obige Diskussion deutet darauf hin, dass es ausreicht, in unserem existenziellen Typ zu speichern. Dies ist auch die Laufzeitdarstellung des Typs, und alles wird in Ordnung sein.

Dies führt uns zur folgenden Implementierung unseres Wrapper-Typs:

 data Dyn where Dyn :: Ord a => TypeRep a -> a -> Dyn toDyn :: (Typeable a, Ord a) => a -> Dyn toDyn val = Dyn (typeOf val) val 

Jetzt schreiben wir eine Funktion, die Folgendes übernimmt:

1. zwei Werte vom Typ Dyn ;
2. eine Funktion, die etwas für zwei Werte eines beliebigen Typs erzeugt ,
   basierend nur auf den Konstanten, die beim Erstellen von Dyn ( forall ist dafür verantwortlich),
   und was aufgerufen wird, wenn beide Dyn Werte des gleichen Typs speichern;
3. und die Fallback-Funktion, die anstelle der vorherigen aufgerufen wird, wenn die Typen noch unterschiedlich sind:

 withDyns :: (forall a. Ord a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn -> Dyn -> b withDyns f def (Dyn ty1 v1) (Dyn ty2 v2) = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2 

SomeTypeRep ist ein existenzieller Wrapper über TypeRep a für ein beliebiges a .

Jetzt können wir zum Beispiel Gleichheitsprüfung und -vergleich implementieren:

 instance Eq Dyn where (==) = withDyns (==) (\_ _ -> False) instance Ord Dyn where compare = withDyns compare compare 

Hier haben wir die Tatsache SomeTypeRep , dass SomeTypeRep miteinander verglichen werden kann, sodass auch die Fallback-Funktion für die Bestellung compare .

Fertig.

Nur jetzt ist es eine Sünde, nicht zu verallgemeinern: Beachten toDyn , withDyns wir in Dyn , toDyn , withDyns Ord speziell verwenden. Dies kann jeder andere Satz von Konstanten sein, sodass wir die ConstraintKinds Erweiterung aktivieren und verallgemeinern können, indem wir Dyn bestimmten Satz von Einschränkungen parametrisieren, die wir verwenden benötigt für unsere spezifische Aufgabe:

 data Dyn ctx where Dyn :: ctx a => TypeRep a -> a -> Dyn ctx toDyn :: (Typeable a, ctx a) => a -> Dyn ctx toDyn val = Dyn (typeOf val) val withDyns :: (forall a. ctx a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn ctx -> Dyn ctx -> b withDyns (Dyn ty1 v1) (Dyn ty2 v2) f def = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2 

Dann ist Dyn Ord unsere Art der Dyn Monoid , und mit Dyn Monoid können Sie beispielsweise beliebige Monoide speichern und mit ihnen etwas Monoidales tun.

Schreiben wir die Instanzen, die wir für unsere neue Dyn benötigen:

 instance Eq (Dyn Eq) where (==) = withDyns (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns compare compare 

... nur das funktioniert nicht. Der Schreibmaschine weiß nicht, dass Dyn Ord auch Eq .
Daher müssen Sie die gesamte Hierarchie kopieren:

 instance Eq (Dyn Eq) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Eq (Dyn Ord) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns d1 d2 compare compare 

Nun sicher.

... vielleicht können Sie es in einem modernen Haskell so gestalten, dass der Timer selbst Instanzen des Formulars anzeigt

 instance C_i (Dyn (C_1, ... C_n)) where ... 

Da dort etwas Prologisches herauskommt, aber ich es noch nicht getan habe, muss ich herum sitzen und es auswählen. Bleib dran.

Und wenn Sie vorsichtig blinzeln, können Sie auch sehen, dass unser Dyn verdächtig aussieht wie ein abhängiges Paar vom Typ (ty : Type ** val : ty) aus den kryptischen Sprachen. Aber nur in mir bekannten Sprachen ist es unmöglich, den Typ zuzuordnen, weil die Parametrizität (die in diesem Fall IMHO zu weit ausgelegt wird), aber hier scheint es möglich.

Aber das Wichtigste - jetzt können Sie sicher etwas wie Map (Dyn Ord) SomeValue und beliebige Werte als Schlüssel verwenden, solange sie selbst den Vergleich unterstützen. Beispielsweise können Bezeichner mit Metrikbeschreibungen als Schlüssel verwendet werden. Dies ist jedoch ein Thema für den nächsten Artikel.