Rekursiv definierte Instanzen und Einschränkungen

Question

Ich habe mit Vektoren und Matrizen gespielt, wo die Größe in ihrem Typ codiert ist, mit der neuen DataKinds Erweiterung. Es geht im Grunde wie folgt:

data Nat = Zero | Succ Nat 

data Vector :: Nat -> * -> * where 
    VNil :: Vector Zero a 
    VCons :: a -> Vector n a -> Vector (Succ n) a 

Jetzt sind wir typische Beispiele wie Functor und Applicative wollen. Functor ist einfach:

instance Functor (Vector n) where 
    fmap f VNil = VNil 
    fmap f (VCons a v) = VCons (f a) (fmap f v) 

Aber mit dem Applicative Beispiel gibt es ein Problem: Wir wissen nicht, welche Art in reinen zurückzukehren. Wir können jedoch die Instanz induktiv auf die Größe des Vektors definieren:

instance Applicative (Vector Zero) where 
    pure = const VNil 
    VNil <*> VNil = VNil 

instance Applicative (Vector n) => Applicative (Vector (Succ n)) where 
    pure a = VCons a (pure a) 
    VCons f fv <*> VCons a v = VCons (f a) (fv <*> v) 

Doch obwohl diese Instanz für alle Vektoren gilt, wird die Typprüfer nicht wissen, so müssen wir die Applicative Einschränkung tragen Jedes Mal, wenn wir die Instanz verwenden.

Nun, wenn dies nur für die Applicative-Instanz gilt, wäre es kein Problem, aber es stellt sich heraus, dass der Trick der rekursiven Instanz Deklarationen wesentlich ist, wenn mit solchen Typen zu programmieren. Zum Beispiel, wenn wir eine Matrix als ein Vektor von Zeilenvektoren unter Verwendung der Bibliothek TypeCompose definieren

type Matrix nx ny a = (Vector nx :. Vector ny) a 

haben wir eine Typ-Klasse zu definieren und rekursive Instanz Erklärungen fügen sowohl die Transponierte und Matrixmultiplikation zu implementieren. Dies führt zu einer enormen Zunahme von Beschränkungen, die wir bei jeder Verwendung des Codes mit sich herumtragen müssen, obwohl die Instanzen tatsächlich für alle Vektoren und Matrizen gelten (wodurch die Beschränkungen nutzlos werden).

Gibt es eine Möglichkeit, all diese Einschränkungen zu vermeiden? Wäre es möglich, den Typenprüfer so zu erweitern, dass er solche induktiven Konstruktionen erkennen kann?

Answer 1

Die Definition von pure steht tatsächlich im Mittelpunkt des Problems. Was sollte sein Typ sein, vollständig quantifiziert und qualifiziert?

pure :: forall (n :: Nat) (x :: *). x -> Vector n x   -- (X) 

nicht tun, da es keine Informationen verfügbar zu Laufzeit ist, um zu bestimmen, ob pureVNil oder VCons emittieren soll. Entsprechend, wie die Dinge stehen, können Sie nicht einfach haben

instance Applicative (Vector n)        -- (X) 

Was können Sie tun? Nun, die Arbeit mit den Strathclyde Haskell Enhancement im Vec.lhs Beispieldatei definiere ich eine Vorstufe pure

vec :: forall x. pi (n :: Nat). x -> Vector {n} x 
vec {Zero} x = VNil 
vec {Succ n} x = VCons x (vec n x) 

mit einem pi Typ, erfordern, dass eine Kopie n zur Laufzeit übergeben werden. Dieser pi (n :: Nat). desugars als

forall n. Natty n -> 

wo Natty mit prosaischem Namen im wirklichen Leben, das Singleton GADT ist von

data Natty n where 
    Zeroy :: Natty Zero 
    Succy :: Natty n -> Natty (Succ n) 

gegeben und die geschweiften Klammern in den Gleichungen für vec übersetzen nur Nat Konstruktoren Natty Konstruktoren.I definieren dann die folgende diabolical Instanz (Umschalten den Standard Functor Instanz off)

instance {:n :: Nat:} => Applicative (Vec {n}) where 
    hiding instance Functor 
    pure = vec {:n :: Nat:} where 
    (<*>) = vapp where 
    vapp :: Vec {m} (s -> t) -> Vec {m} s -> Vec {m} t 
    vapp VNil   VNil   = VNil 
    vapp (VCons f fs) (VCons s ss) = VCons (f s) vapp fs ss 

die weite Technologie verlangt, immer noch. Die Einschränkung {:n :: Nat:} desugars zu etwas, das erfordert, dass ein Natty n Zeuge existiert, und durch die Macht der Variablen des Bereichs, die gleichen {:n :: Nat:} Unterpojen, die explizit zeugen. Langschrift, das ist

class HasNatty n where 
    natty :: Natty n 
instance HasNatty Zero where 
    natty = Zeroy 
instance HasNatty n => HasNatty (Succ n) where 
    natty = Succy natty 

und wir ersetzen die Einschränkung {:n :: Nat:} mit HasNatty n und den entsprechenden Begriff mit (natty :: Natty n). Diese Konstruktion führt systematisch dazu, ein Fragment eines Haskell-Typcheckers in der Typklasse Prolog zu schreiben, was nicht meine Vorstellung von Freude ist, also benutze ich einen Computer.

Beachten Sie, dass die Traversable Instanz (mein Idiom Klammern und mein stilles Standard Functor und faltbare Instanzen verzeihen) erfordert keine solche jiggery pokery

instance Traversable (Vector n) where 
    traverse f VNil   = (|VNil|) 
    traverse f (VCons x xs) = (|VCons (f x) (traverse f xs)|) 

Das ist alles, die Struktur, die Sie brauchen Matrix-Multiplikation zu erhalten, ohne weitere explizite Rekursion.

TL; DR Verwenden Sie die Singleton-Konstruktion und die ihr zugeordnete Typklasse, um alle rekursiv definierten Instanzen in die Existenz eines Laufzeitzeugen für die Daten auf Textebene zu zerlegen, aus denen Sie durch explizite Rekursion berechnen können.

Welche Auswirkungen hat das Design?

GHC 7.4 hat die Art Förderung Technologie, aber sie hat immer noch die Singleton-Konstruktion pi-Typen zu bieten. Eine eindeutig wichtige Sache über promotierte Datentypen ist, dass sie geschlossen sind, aber das zeigt sich nicht wirklich sauber: die Konstruierbarkeit von Singleton-Zeugen ist die Manifestation dieser Geschlossenheit. Irgendwie, wenn Sie forall (n :: Nat). haben, dann ist es immer sinnvoll, ein Singleton zu verlangen, aber dies zu tun, macht einen Unterschied zum generierten Code: ob es explizit wie in meinem pi Konstrukt oder implizit wie im Wörterbuch für {:n :: Nat:} ist, gibt es extra Laufzeitinformation zum Umherlegen und ein entsprechend schwächerer freier Satz.

Eine offene Entwurfsfrage für zukünftige Versionen von GHC ist, wie diese Unterscheidung zwischen dem Vorhandensein und dem Fehlen von Laufzeitzeugen für Daten auf Typenebene verwaltet wird. Auf der einen Seite brauchen wir sie in Zwängen. Auf der anderen Seite müssen wir Pattern-Match auf ihnen. Z. B. sollte pi (n :: Nat). bedeuten die explizite

forall (n :: Nat). Natty n -> 

oder die implizite

forall (n :: Nat). {:n :: Nat:} => 

? Natürlich haben Sprachen wie Agda und Coq beide Formen, also sollte Haskell vielleicht folgen. Es gibt sicherlich Raum für Fortschritte, und wir arbeiten daran!