Was genau sind GHC-Typ-Koerzitien?

Question

Ich habe nach Haskells Kernsprache gesucht, um zu verstehen, wie es funktioniert. Ein Merkmal, das ich bei meinen Internet-Recherchen fand, waren Schreibzwänge. Ich weiß, dass sie verwendet werden, um GADTs zu implementieren, aber ich verstehe nicht viel anderes. Alle Beschreibungen, die ich online fand, waren ziemlich hoch für mich, obwohl ich ein ordentliches Verständnis von System F habe. Kann mir bitte bitte Typzwange auf verständliche Art erklären?

Answer 1

Grundsätzlich kompiliert Haskell durch Auswertung zu dieser einfachen Kernsprache. In dem Bemühen, einfach zu bleiben, ist es im Allgemeinen nicht wünschenswert, Konstrukte wie GADTs oder Typklassen direkt der Sprache hinzuzufügen, sondern stattdessen am vorderen Ende des Compilers in die einfacheren, aber allgemeineren (und ausführlichen) Konstrukte kompiliert zu werden Ader. Denken Sie auch daran, dass Core typisiert ist, so dass wir sicherstellen müssen, dass wir all diese Dinge typisiert codieren können, was eine erhebliche Komplikation darstellt.

Um GADTs zu codieren, werden sie zu normalen Datentypen mit Existenzialen und Zwängen ausgearbeitet. Die Grundidee ist, dass ein Zwang ein Typ mit einer sogenannten Gleichheitsart ist, geschrieben t ~ t'. Dieser Typ soll Beweise bezeugen, dass, obwohl wir es vielleicht nicht wissen, t und t' vom gleichen Typ unter der Haube sind. Sie werden herumgereicht wie jeder andere Typ, also ist nichts Besonderes darin, wie das gehandhabt wird. Es gibt auch eine Reihe von Typkonstruktoren zur Manipulation dieser Typen, die kleine Beweise über die Gleichheit liefern, wie zum Beispiel sym :: t ~ t' -> t' ~ t. Schließlich gibt es einen Operator auf der Benennungsebene, der eine Benennung des Typs t und eine Art der Art t ~ t' verwendet und als Benennung des Typs t' eingegeben wird. zB cast e T :: t', aber dieser Begriff verhält sich identisch zu e. Wir haben gerade unseren Beweis verwendet, dass t' und t gleich sind, um e zu werfen, um den Typüberprüfer glücklich zu machen.

, dass die Grundidee

cast auf dem Begriff Ebene

• Kinds darstellt Gleichheit
• Typen, die Beweise für die Gleichstellung ist diese Beweise

Auch verwenden beachten Sie, dass durch Beweise zu isolieren die Typ-Ebene kann nicht mit Laufzeitkosten enden, da die Typen auf der ganzen Linie gelöscht werden.

Ich denke, eine nette Referenz auf all das ist System F with Type Equality Coercions, aber natürlich alle SPJ-Publikationen könnten helfen.

Answer 2

@jozefg verdient die Antwort, aber hier ist ein Beispiel von GADTs, die sich zur existenziellen Quantifizierung entschließen. Noch nicht ganz Core, aber ein Schritt dazu.

data Foo :: * -> * where 
    Bar :: Int -> Foo Int 
    Oink :: b -> c -> d -> Foo (f b) 

über

data Foo a where 
    Bar :: (a ~ Int) => Int -> Foo a 
    Oink :: (a ~ f b) => b -> c -> d -> Foo a 

zu

data Foo a 
    = (a ~ Int) => Bar Int 
    | forall b c d f. (a ~ f b) => Oink b c d 

mit freundlicher Genehmigung von /u/MitchellSalad on /r/haskell.