In der Haskell-Community fügen wir langsam Funktionen abhängiger Typen hinzu. Abhängige Typen ist eine erweiterte Tippfunktion, mit der Arten von Werten abhängen können. Einige Sprachen wie Agda und Idris haben sie bereits. Es scheint ein sehr fortgeschrittenes Feature zu sein, das ein erweitertes Typsystem erfordert, bis Sie feststellen, dass Python abhängige Typen hatte die dynamische Typisierung abhängiger Typen, die tatsächlich abhängige Typen sein können oder nicht, von Anfang an.
Für fast jedes Programm in einer funktionalen Programmiersprache gibt es eine Möglichkeit, es als untypisierten Lambda-Kalkül-Begriff zu wiederholen, egal wie fortgeschritten die Typisierung ist. Das liegt daran, dass durch das Eintippen nur Programme eliminiert, neue nicht aktiviert werden.
Strong Typing gewinnt uns Sicherheit. Wie Klassen von Fehlern, die zur Laufzeit stattfanden, zur Laufzeit nicht mehr auftreten können. Diese Sicherheit ist ziemlich nett. Abgesehen von dieser Sicherheit, was gibt dir starkes Tippen?
Gibt es neben der Sicherheit noch weitere Vorteile eines starken Systemtyps?
(Beachten Sie, dass ich nicht sage, dass starkes Tippen wertlos ist. Sicherheit ist ein großer Nutzen für sich. Ich frage mich nur, ob es weitere Vorteile gibt.)
Zuerst müssen wir ein wenig über die Geschichte des einfach typisierten Lambda-Kalküls sprechen.
Es gibt zwei historische Entwicklungen des einfach typisierten Lambda-Kalküls.
Als Alonzo Church den Lambda-Kalkül beschrieb, wurden die Typen als Teil des Bedeutungs- / Betriebsverhaltens der Begriffe gebacken.
Als Haskell Curry den Lambda-Kalkül beschrieb, waren die Typen Anmerkungen zu den Begriffen.
Also haben wir den Lambda-Kalkül a la Church und den Lambda-Kalkül a la Curry. Siehe Ссылка für mehr.
Ironischerweise basiert die Sprache Haskell, die nach Curry benannt ist, auf einem Lambda-Kalkül a la Church!
Was das bedeutet, sind die Typen nicht einfach Annotationen, die schlechte Programme für Sie ausschließen. Sie können auch "Sachen machen". Solche Typen löschen nicht, ohne Rückstände zu hinterlassen.
Das zeigt sich in Haskells Vorstellung von Typenklassen, und das ist der Grund, warum Haskell eine Sprache a la Kirche ist.
In Haskell, wenn ich eine Funktion mache
%Vor% Wir übergeben ein Objekt oder ein Wörterbuch für Ord a als erstes Argument.
Aber Sie sind nicht gezwungen, dieses Argument um sich herum im Code auszuloten, es ist die Aufgabe des Compilers, das aufzubauen und zu benutzen.
%Vor%Wenn Sie also eine Liste von Strings sortieren, die selbst Listen von Zeichen sind, dann baut dies das Wörterbuch auf, indem es die Ord Char-Instanz durch die Instanz für Ord a = & gt; Ord [a], um Ord [Char] zu erhalten, was dasselbe wie Ord String ist, dann können Sie eine Liste von Strings sortieren.
Der Aufruf von sort oben ist viel weniger ausführlich als das manuelle Erstellen eines LexicographicComparator<List<Char>> , indem Sie ihm einen IComparator<Char> an seinen Konstruktor übergeben und die Funktion mit einem zusätzlichen zweiten Argument aufrufen, wenn ich die Komplexität des Aufrufs vergleichen sollte eine solche sort -Funktion in Haskell, um sie in C # oder Java aufzurufen.
Dies zeigt uns, dass die Programmierung mit Typen wesentlich weniger ausführlich sein kann, weil Mechanismen wie implicits und typeclasses einen großen Teil des Codes für Ihr Programm während der Typprüfung ableiten können.
Auf einer einfacheren Basis können sogar die Größen von Argumenten von Typen abhängen, es sei denn, Sie wollen ziemlich hohe Kosten dafür bezahlen, alles in Ihrer Sprache zu verpacken, so dass es eine homogene Darstellung hat.
Dies zeigt uns, dass das Programmieren mit Typen wesentlich effizienter sein kann, da es dedizierte Darstellungen verwenden kann, anstatt überall in Ihrem Code geboxte Strukturen zu bezahlen. Ein int kann nicht einfach eine Maschinen-Ganzzahl sein, weil es irgendwie wie alles andere im System aussehen muss. Wenn Sie bereit sind, zur Laufzeit eine Größenordnung oder mehr Leistung aufzugeben, ist dies für Sie nicht von Bedeutung.
Schließlich, wenn wir Typen haben, die "Dinge tun" für uns, ist es oft vorteilhaft, die Refactoring-Vorteile zu berücksichtigen, die reine Sicherheit bietet.
Wenn ich den kleineren Satz Code, der übrig bleibt, umgestalte, schreibt er alle diese Klöster der Typklasse für mich neu. Es wird herausfinden, wie es den Code neu schreiben kann, um mehr Argumente zu entpacken. Ich bin nicht damit beschäftigt, all diese Dinge mit der Hand auszuarbeiten, ich kann diese alltäglichen Aufgaben dem Typ-Checker überlassen.
Aber selbst wenn ich die Typen ändere, kann ich argwöhnisch Argumente umherbewegen, angenehm, dass der Compiler sehr wahrscheinlich meine Fehler fängt. Typen geben Ihnen "freie Sätze", die wie Unit-Tests für ganze Klassen solcher Fehler sind.
Auf der anderen Seite, sobald ich eine API in einer Sprache wie Python gesperrt habe, habe ich Todesangst davor, sie zu ändern, weil sie zur Laufzeit stillschweigend für alle meine Downstream-Abhängigkeiten bricht! Dies führt zu barocken APIs, die sich stark auf leicht verrottete Schlüsselwort-Argumente stützen, und die API von etwas, das sich im Laufe der Zeit entwickelt, ähnelt kaum dem, was Sie aus der Box heraus bauen würden, wenn Sie es noch einmal machen müssten. Folglich haben selbst die reinen Sicherheitsbedenken langfristige Auswirkungen auf das API-Design, sobald Sie möchten, dass die Leute auf Ihrer Arbeit aufbauen, anstatt sie einfach zu ersetzen, wenn es zu unhandlich wird.
Das liegt daran, dass durch das Eintippen nur Programme eliminiert, neue nicht aktiviert werden.
Dies ist keine korrekte Aussage. Typklassen ermöglichen es, Teile Ihres Programms aus Informationen auf Typenebene zu generieren.
Betrachte zwei Ausdrücke:
readMaybe "15" :: Maybe Integer readMaybe "15" :: Maybe Bool Hier verwende ich die Funktion readMaybe aus dem Modul Text.Read . Auf Termebene sind diese Ausdrücke identisch, nur ihre Typanmerkungen sind unterschiedlich. Die Ergebnisse, die sie zur Laufzeit erzeugen, unterscheiden sich jedoch ( Just 15 im ersten Fall, Nothing im zweiten Fall).
Dies liegt daran, dass der Compiler Code aus den statischen Informationen generiert, die Sie haben. Um genauer zu sein, wählt es eine geeignete Klasseninstanz aus und übergibt ihr Wörterbuch an die polymorphe Funktion ( readMaybe in unserem Fall).
Dieses Beispiel ist einfach, aber es gibt wesentlich komplexere Anwendungsfälle. Mit der Bibliothek mtl können Sie Berechnungen schreiben, die in verschiedenen Berechnungskontexten ausgeführt werden (aka Monad s). Der Compiler fügt automatisch eine Menge Code ein, der die Berechnungskontexte verwaltet. In einer dynamisch typisierten Sprache hätten Sie keine statischen Informationen, um dies zu ermöglichen.
Wie Sie sehen, schneidet die statische Typisierung nicht nur falsche Programme ab, sondern schreibt auch richtige für Sie.
Refactoring. Mit einem starken Typsystem können Sie Code sicher umgestalten und der Compiler Ihnen mitteilen, ob das, was Sie gerade tun, jetzt sogar Sinn macht. Je stärker das Typisierungssystem, desto mehr Refactor-Fehler werden vermieden. Dies bedeutet natürlich, dass Ihr Code viel wartbarer ist.
Sie brauchen "Sicherheit", wenn Sie bereits wissen, was und wie Sie schreiben möchten. Es ist ein sehr kleiner Teil dessen, für welche Arten nützlich sind. Das Wichtigste an Typen ist, dass sie Ihr Denken strukturieren. Wenn jemand in Python a + b schreibt, sieht er a und b nicht als abstrakte Variablen - er sieht sie als Zahlen. Typen gibt es bereits in der internen Sprache des Menschen, Python hat einfach kein Typsystem, um darüber zu sprechen. Die eigentliche Frage in dem Streit um "typisierte gegen untypisierte (uneinheitliche) Programmierung" lautet: "Wollen wir unsere internen strukturierten Konzepte auf sichere und explizite oder unsichere und implizite Weise widerspiegeln?". Typen führen keine neuen Konzepte ein - es ist eine untypische Argumentation, die die bestehenden vergisst.
Wenn jemand auf einen Baum schaut (ich meine einen wirklich grünen), sieht er nicht jedes einzelne Blatt darauf, aber er behandelt es auch nicht als abstraktes, namenloses Objekt. "Ein Baum" - ist eine Annäherung, die für die meisten Fälle gut genug ist, und deshalb haben wir Systeme vom Typ Hindley-Milner, aber manchmal möchten Sie über einen bestimmten Baum sprechen und Sie möchten sich die Blätter ansehen. Und das gibt dir abhängige Typen: die Fähigkeit zu zoomen. "Ein Baum ohne Blätter", "ein Baum im Wald", "ein Baum in einer bestimmten Form" ... Abhängige Programmierungen sind nur ein weiterer Schritt in Richtung des menschlichen Denkens.
In einer weniger abstrakten Notiz habe ich einen Typ-Checker für eine Spielzeug-abhängige Typ-Sprache, wo alle Typisierungsregeln als Konstruktoren eines Datentyp . Sie müssen nicht in die Typprüfung eintauchen, um die Regeln des Systems zu verstehen. Das ist die Kraft des "Zoomens": Sie können so komplexe Invarianten einführen, wie Sie wollen, und so wesentliche Teile von nicht wichtigen unterscheiden.
Ein weiteres Beispiel für die leistungsabhängigen Typen gibt Ihnen verschiedene Formen der Reflexion. Schaue z.B. in der Pierre-Évariste Dagand Thesis , was beweist, dass
generische Programmierung ist nur Programmierung
Und natürlich sind Typen Andeutungen, viele Funktionen und Abstraktionen, die ich definiert habe, würde ich viel ungeschickter in einer schwach typisierten Sprache definieren, aber Typen haben bessere Alternativen vorgeschlagen.
Es gibt einfach keine Frage "Was soll ich wählen: einfache Typen oder abhängige Typen?". Abhängige Typen sind immer besser und sie umfassen natürlich einfache Typen. Die Frage ist "Was zu wählen: keine Typen oder abhängigen Typen?", Aber diese Frage steht nicht für mich.
Tags und Links haskell functional-programming types dependent-type type-systems