Ein Typkonstruktor erzeugt einen Typ mit einem gegebenen Typ. Zum Beispiel der Maybe-Konstruktor
%Vor%könnte ein konkreter Typ wie Char sein und einen konkreten Typ wie Maybe Char geben. In Bezug auf Arten hat man
%Vor%Meine Frage: Ist es möglich, einen Typkonstruktor zu definieren, der einen konkreten Typ mit Char liefert? Anders ausgedrückt, ist es möglich, Arten und Typen in der Typunterschrift eines Typkonstruktors zu mischen? Etwas wie
%Vor%Kann ein Konstruktor vom Typ Haskell nicht-type Parameter haben?
Lassen Sie uns entpacken, was Sie mit type Parameter meinen. Das Wort type hat (mindestens) zwei mögliche Bedeutungen: meinst du typ im engeren Sinn von Dingen der Art * , oder im weiteren Sinn von Dingen auf der Typ-Ebene ? Wir können (noch) keine Werte in Typen verwenden, aber das moderne GHC verfügt über eine sehr reichhaltige Sprache, die es uns erlaubt, eine Vielzahl anderer Dinge als konkrete Typen als Typparameter zu verwenden.
Typkonstruktoren in Haskell haben immer nicht * -Parameter zugelassen. Zum Beispiel funktioniert die Kodierung des Fixpunktes eines Funktors in reinem alten Haskell 98:
Fix wird von einem Funktor vom Typ * -> * parametrisiert, nicht vom Typ * .
* und ->
Die Erweiterung DataKinds bereichert das GHC-System um vom Benutzer deklarierte Arten. Daher können Arten aus anderen Teilen als * und -> erstellt werden. Es funktioniert, indem alle data -Deklarationen auf die Art-Ebene hochgestuft werden. Das heißt, eine data Deklaration wie
führt einen Art Nat und Typ Konstruktoren Z :: Nat und S :: Nat -> Nat ein, sowie die üblichen Typ- und Wertkonstruktoren. Auf diese Weise können Sie Datentypen schreiben, die durch Daten auf Typenebene parametrisiert sind, z. B. der übliche Vektor vector , bei dem es sich um eine verkettete Liste handelt, die durch ihre Länge indiziert wird.
Es gibt eine verwandte Erweiterung namens ConstraintKinds , die Constraints wie Ord a vom Joch des "fetten Pfeils" => befreit und es ihnen ermöglicht, sich durch die Landschaft des Typsystems zu bewegen, wie es die Natur beabsichtigt hat. Kmett hat diese Fähigkeit genutzt, um eine Kategorie von Einschränkungen zu erstellen, mit dem newtype (:-) :: Constraint -> Constraint -> * bezeichnet "failibility": ein Wert vom Typ c :- d ist ein Beweis, dass, wenn c gilt, auch d gilt. Zum Beispiel können wir beweisen, dass Ord a Eq [a] für alle a bedeutet:
forall
Haskell unterhält derzeit jedoch eine strikte Trennung zwischen Typ- und Wertebene. Dinge auf der Typ-Ebene werden immer gelöscht, bevor das Programm läuft, (fast) immer ableitbar, in Ausdrücken unsichtbar und (abhängig) durch forall quantifiziert. Wenn Ihre Anwendung etwas flexibleres erfordert, z. B. die abhängige Quantifizierung von Laufzeitdaten, müssen Sie sie manuell mit einer Singleton -Encodierung simulieren.
Zum Beispiel sagt die Spezifikation von split , dass es einen Vektor mit einer bestimmten Länge entsprechend seinem Argument (Laufzeit!) zerhackt. Der Typ des Ausgabevektors hängt vom Wert des Arguments split ab. Wir würden das gerne schreiben ...
... wo ich die Typefunktion (:+:) :: Nat -> Nat -> Nat verwende, die für das Hinzufügen von Typenniveausaturals steht, um sicherzustellen, dass der Eingabevektor mindestens so lang ist wie n ...
... aber Haskell wird diese Deklaration von split nicht zulassen! Es gibt keine Werte vom Typ Z oder S n ; Nur Typen vom Typ * enthalten Werte. Wir können nicht direkt auf n zur Laufzeit zugreifen, aber wir können eine GADT verwenden, auf die wir eine Musterübereinstimmung mit lerne für die Typ-Ebene n haben:
Natty wird ein Singleton genannt, weil es für eine gegebene (gut definierte) n nur einen (wohldefinierten) Wert vom Typ Natty n gibt. Wir können Natty n als Laufzeit-Unterstützung für n verwenden.
Wie auch immer, der Punkt ist, dass Werte - Laufzeitdaten - nicht in Typen vorkommen können. Es ist ziemlich mühsam, die Definition von Nat in Singleton-Form zu duplizieren (und die Dinge werden schlimmer, wenn der Compiler solche Werte ableiten soll); abhängig typisierte Sprachen wie Agda, Idris oder ein zukünftiger Haskell entziehen sich der Tyrannei, Typen strikt von Werten zu trennen und geben uns eine Reihe expressiver Quantoren. Sie sind in der Lage, ein Laufzeitargument% html Nat as split zu verwenden und dessen Wert abhängig vom Rückgabetyp anzugeben.
@pigworker hat ausführlich über die Unangemessenheit von Haskells strikter Trennung zwischen Typen und Werten für moderne abhängige Programmierung geschrieben. Siehe zum Beispiel das Hasochism Papier , oder seine Diskussion über die ungeprüften Annahmen, die uns von vier Jahrzehnten Hindley-Milner-Stil-Programmierung eingetrichtert wurden.
Schließlich, was es wert ist, mit TypeInType modern GHC vereinheitlicht Typen und Arten, so dass wir über Art Variablen mit den gleichen Werkzeugen sprechen können, die wir verwenden, um über Typvariablen zu sprechen. In einem früheren Post über Sitzungstypen habe ich TypeInType verwendet, um eine Art für getaggte type-level Sequenzen von Typen zu definieren :
Ich würde @ Benjamin Hodgson's Antwort und die Referenzen, die er gibt, um zu sehen, wie man diese Art von Ding nützlich macht , empfehlen. Um Ihre Frage direkter zu beantworten und mehrere Erweiterungen ( DataKinds , KindSignatures und GADTs ) zu verwenden, können Sie Typen definieren, die auf (bestimmten) konkreten Typen parametrisiert sind.
Hier ist zum Beispiel eine für den konkreten Bool -Datentyp parametrisiert:
Beachten Sie, dass sich dies nicht wesentlich von der Definition zweier völlig getrennter Typen unterscheidet:
%Vor% Tatsächlich fällt es mir schwer, an irgendeinen Vorteil zu denken, den Flagged gegenüber dem Definieren von zwei separaten Typen hat, außer wenn Sie mit jemandem in einer Bar wetten, dass Sie nützlichen Haskell-Code ohne Klassen schreiben können. Zum Beispiel können Sie schreiben:
Vielleicht kann jemand anderes an andere Vorteile denken.
Wie auch immer, ich glaube, dass das Parametrisieren von Typen mit konkreten Werten nur dann sinnvoll ist, wenn der konkrete Typ "reich" genug ist, um den Typ-Checker zu nutzen, wie in Benjamins Beispielen.
Wie @ user2407038 bemerkt, können die meisten interessanten primitiven Typen wie Int s, Char s, String s usw. nicht auf diese Weise verwendet werden. Interessanterweise können Sie jedoch > wörtliche positive Ganzzahlen und Strings als Typparameter verwenden, aber sie werden als Nat s und Symbol s (wie in GHC.TypeLits definiert) behandelt.
So etwas ist möglich:
%Vor%Sehen Sie sich die Verwendung generalisierter algebraischer Datentypen (GADTS) an, die es Ihnen ermöglichen, konkrete Ausgaben basierend auf dem Eingabetyp zu definieren, z.
%Vor%Zu einem ähnlichen Effekt können RankNTypes die Implementierung von ähnlichem Verhalten ermöglichen:
%Vor%Die PolyType-Definition ermöglicht es Ihnen, die polymorphe Funktion in exampleFunctionTwo einzufügen und ihre Ausgabe auf 'Int' zu setzen.
Nein. Haskell hat (noch) keine abhängigen Typen. Siehe Ссылка für eine Diskussion darüber, wann es möglich ist.
In der Zwischenzeit kann man sich in Agda, Idris und Cayenne so verhalten.