Was macht das Typsystem von Haskell mächtiger als das Typsystem anderer Sprachen?

Question

Beim Lesen von Nachteile des Scala-Typsystems gegenüber Haskell? muss ich fragen: Was ist es speziell, das das Typsystem von Haskell mächtiger macht als die Typsysteme anderer Sprachen (C, C ++, Java)? Anscheinend kann selbst Scala einige der gleichen Funktionen wie das Typsystem von Haskell nicht ausführen. Was ist es speziell, das das Typsystem von Haskell (Hindley-Milner Typinferenz) so mächtig macht? Kannst du ein Beispiel geben?

Answer 1

Was ist es speziell, das das Typsystem von Haskell ausmacht

Es wurde im Laufe des letzten Jahrzehnts entwickelt, um sowohl flexibel -- als Logik für die Eigenschaftsüberprüfung -- als auch leistungsstark zu sein.

Das Typsystem von Haskell wurde im Laufe der Jahre entwickelt, um eine relativ flexible, ausdrucksstarke statische Prüfdisziplin zu fördern, wobei mehrere Gruppen von Forschern Typsystemtechniken identifizierten, die leistungsstarke neue Klassen von Kompilierzeit-Verifizierungen ermöglichen. Das von Scala ist in diesem Bereich relativ unterentwickelt.

Das heißt, Haskell/GHC bietet eine Logik, die sowohl leistungsstark als auch darauf ausgelegt ist, die Programmierung auf Typenebene zu fördern. Etwas ziemlich einzigartiges in der Welt der funktionalen Programmierung.

Einige Arbeiten, die einen Eindruck von der Richtung vermitteln, in die die Entwicklung des Typsystems von Haskell gegangen ist:

• Vergnügen mit Typfunktionen
• Assoziierte Typen mit Klasse
• Vergnügen mit funktionalen Abhängigkeiten

Answer 2

Hindley-Milner ist kein Typsystem, sondern ein Typinferenzalgorithmus. Das Typsystem von Haskell konnte früher vollständig mit HM inferiert werden, aber für das moderne Haskell mit Erweiterungen ist dieses Schiff längst abgesegelt. (ML bleibt in der Lage, vollständig inferiert zu werden).

Argumentierbar gibt die Fähigkeit, hauptsächlich oder vollständig alle Typen zu inferieren, Macht in Bezug auf Ausdruckskraft.

Aber das ist größtenteils nicht, worum es meiner Meinung nach wirklich geht.

Die von dons verlinkten Papers weisen auf den anderen Aspekt hin - dass die Erweiterungen des Typsystems von Haskell es Turing-vollständig machen (und moderne Typfamilien diese Turing-vollständige Sprache viel stärker an die Programmierung auf Werte-Ebene anlehnen lassen). Ein weiteres interessantes Paper zu diesem Thema ist McBrides Vortäuschen: Simulation abhängiger Typen in Haskell.

Das Paper im anderen Thread zu Scala: "Typklassen als Objekte und Implizite" geht darauf ein, warum du tatsächlich auch die meisten dieser Dinge in Scala machen kannst, wenn auch mit etwas mehr Explizitheit. Ich neige dazu zu glauben, aber das beruht mehr auf einem Bauchgefühl als auf echter Scala-Erfahrung, dass der eher ad-hoc und explizite Ansatz (was die C++-Diskussion als "nominal" bezeichnet hat) letztendlich etwas unordentlicher ist.

Answer 3

Lasst uns mit einem sehr einfachen Beispiel weitermachen: Haskell's Maybe.

data Maybe a = Nothing | Just a

In C++:

template 
struct Maybe {
    bool isJust;
    T value;  // WICHTIG: ignorieren, wenn !isJust
};

Betrachten wir diese beiden Funktionssignaturen, in Haskell:

sumJusts :: Num a => [Maybe a] -> a

und in C++:

template  T sumJusts(vector >);

Unterschiede:

• In C++ gibt es mehr mögliche Fehler, die gemacht werden können. Der Compiler überprüft die Verwendungsregel von Maybe nicht.
• Der C++ Typ von sumJusts gibt nicht an, dass er + benötigt und von 0 castet. Die Fehlermeldungen, die erscheinen, wenn Dinge nicht funktionieren, sind kryptisch und seltsam. In Haskell wird der Compiler einfach bemängeln, dass der Typ keine Instanz von Num ist, sehr unkompliziert.

Kurz gesagt, Haskell hat:

• ADTs
• Typklassen
• Eine sehr benutzerfreundliche Syntax und gute Unterstützung für Generics (die in C++ von Leuten gemieden werden, wegen all ihrer Kryptizität)

Answer 4

Die Haskell-Sprache ermöglicht es Ihnen, sichereren Code zu schreiben, ohne auf Funktionalitäten verzichten zu müssen. Die meisten Sprachen tauschen heutzutage Features gegen Sicherheit: Die Haskell-Sprache zeigt, dass es möglich ist, beides zu haben.

Wir können ohne Null-Pointer, explizite Umwandlungen und lockere Typisierung auskommen und dennoch eine perfekt ausdrucksstarke Sprache haben, die in der Lage ist, effizienten Endcode zu erzeugen.

Darüber hinaus gibt Ihnen das Haskell-Typsystem in Verbindung mit seinem standardmäßig faulen und reinen Ansatz zum Codieren einen Schub bei komplizierten, aber wichtigen Themen wie Parallelität und Nebenläufigkeit.

Nur meine zwei Cent.

Answer 5

Etwas, was ich wirklich mag und in anderen Sprachen vermisse, ist die Unterstützung von Typklassen, die eine elegante Lösung für viele Probleme darstellen (einschließlich zum Beispiel polyvariate Funktionen).

Mit Typklassen ist es äußerst einfach, sehr abstrakte Funktionen zu definieren, die trotzdem vollständig typsicher sind - wie zum Beispiel diese Fibonacci-Funktion:

fibs :: Num a => [a]
fibs@( _ :xs) = 0:1:zipWith (+) fibs xs

Zum Beispiel:

map (`div` 2) fibs        -- integraler Kontext
(fibs !! 10) + 1,234      -- rationaler Kontext
map ( :+ 1,0) fibs         -- Komplexer Kontext

Sie können sogar Ihren eigenen numerischen Typ dafür definieren.