Motivation für die Beschränkung der Förderung von Daten

Question

Könnte jemand die Motivation hinter dem Grenzwert für die Förderung von Datentypen, der in Abschnitt 7.9.2 of the GHC user guide diskutiert wird, erklären oder erraten?

Die folgenden Einschränkungen gelten für die Förderung:

• Wir haben leider nur Datentypen, deren Arten fördern, sind von der Form * -> ... -> * -> *. Insbesondere fördern wir keine höherwertigen Datentypen wie data Fix f = In (f (Fix f)) oder Datentypen, deren Arten promoted Typen wie Vec :: * -> Nat -> * betreffen.

Insbesondere ist ich in dem letzten Bit über geförderte Typen wie Vec :: * -> Nat -> * interessiert. Einige Arten wie diese zu fördern scheint natürlich. Ich lief sehr schnell in es, während ich versuchte, eine meiner Bibliotheken zu konvertieren, um bestimmte geförderte Arten für die verschiedenen Phantom-Typen zu verwenden, statt die Art * für alles zu verwenden, um bessere Dokumentation und dergleichen bereitzustellen.

Oft die Gründe für Compiler Einschränkungen wie diese springen auf Sie mit ein wenig Nachdenken, aber ich sehe das nicht. Ich frage mich also, ob es in der Kategorie "noch nicht gebraucht, also wir haben es nicht gebaut" oder "das ist unmöglich/unentscheidbar/zerstört Inferenz" kommt.

Answer 1

Eine interessante Sache passiert, wenn Sie Arten fördern, die durch beförderte Typen indiziert werden. Stellen Sie sich vor wir

data Nat = Ze | Su Nat 

und dann

data Vec :: Nat -> * -> * where 
    VNil :: Vec Ze x 
    VCons :: x -> Vec n x -> Vec (Su n) x 

Hinter den Kulissen, die internen Arten der Konstrukteure stellen die instanziiert-Return-Indizes durch Einschränkungen bauen, als ob wir

data Vec (n :: Nat) (a :: *) 
    =   n ~ Ze => VNil 
    | forall k. n ~ Su k => VCons a (Vec k a) 

geschrieben hatte,

Nun, wenn wir etwas wie

erlaubt wurden

data Elem :: forall n a. a -> Vec n a -> * where 
    Top :: Elem x (VCons x xs) 
    Pop :: Elem x xs -> Elem x (VCons y xs) 

die Übersetzung innere Form hätte so etwas wie

data Elem (x :: a) (zs :: Vec n a) 
    = forall (k :: Nat), (xs :: Vec k a).   (n ~ Su k, zs ~ VCons x xs) => 
     Top 
    | forall (k :: Nat), (xs :: Vec k s), (y :: a). (n ~ Su k, zs ~ VCons y xs) => 
     Pop (Elem x xs) 

aber an der zweiten Einschränkung in jedem Fall zu sehen sein!Wir haben

zs :: Vec n a 

aber

VCons x xs, VCons y xs :: Vec (Su k) a 

Aber im System FC als dann definiert, Gleichheitsbeschränkungen Arten von der gleichen Art auf beiden Seiten haben muss, so ist dieses Beispiel nicht unbeträchtlich problematisch.

Eine Lösung ist, die Beweise für die erste Bedingung verwenden, um die zweite zu reparieren, aber dann würden wir abhängig Zwänge

(q1 :: n ~ Su k, zs |> q1 ~ VCons x xs) 

müssen, ist Ein weiterer Fix nur heterogene Gleichungen zu ermöglichen, wie ich in den abhängigen Art tat Theorie vor fünfzehn Jahren. Es wird unvermeidlich Gleichungen zwischen Dingen geben, deren Arten auf eine Art und Weise gleich sind, die nicht syntaktisch offensichtlich ist.

Es ist der letztere Plan, der derzeit bevorzugt wird. Soweit ich weiß, wurde die von Ihnen genannte Politik als Holdingposition angenommen, bis das Design für eine Kernsprache mit heterogener Gleichheit (wie von Weirich und seinen Kollegen vorgeschlagen) zur Umsetzung gereift ist. Wir leben in interessanten Zeiten.

Answer 2

Dies ergibt sich wohl aus der Tatsache, dass GHC hat keine besonders reiche Begriff „Art“, sortiert die Art der Arten sind, so

values : type : kind : sort : ... 

Beachten Sie, dass, während wir ein ziemlich kompliziertes System von Arten mit Datenarten, alle Arten fördern noch zu sehr einfachen Sortierungen. Die Förderung von Arten wie Nat würde erfordern, dass es mehr als einen Sortiertyp/Konstruktor gibt, und die Förderung Fix würde höhere sortierte Arten erfordern, was ebenfalls nicht im primitiven Sortiersystem enthalten ist.

Dies ist keine technische Barriere, Sprachen wie Coq oder Agda (abhängig typisierte Sprachen) haben einen ganzen unendlichen Stapel von diesen, aber GHC ist erst kürzlich ein freundliches System gewachsen. Es ist noch kein ausgeklügeltes Sortiersystem implementiert, vielleicht werden wir in Zukunft einen bekommen.