Soweit ich weiß, wird jede Programmiersprache, die beim Schreiben einer Funktion oder eines Moduls keine Typanmerkungen in die Quelle schreiben muss und wenn dieser Teil des Codes "type-correct" ist, Compiler die Typen und Kompilierungen ableiten der Code. gibt es mehr dazu?
gibt es eine solche Sprache (n)? Wenn ja, gibt es irgendwelche Einschränkungen für das Typsystem?
Update 1: Nur um wirklich klar zu sein, frage ich nach einer statisch typisierten, voll typus-abgeleiteten Programmiersprache, nicht einer dynamisch typisierten Programmiersprache.
Die Einschränkung der vollständigen Typ-Inferenz besteht darin, dass sie nicht mit vielen erweiterten Systemfunktionen funktioniert. Als ein Beispiel betrachten Haskell und OCaml. Beide Sprachen sind fast vollständig typabgeleitet, haben aber einige Merkmale, die die Typinferenz beeinflussen können.
In Haskell gibt es Typklassen kombiniert mit polymorphen Rückgabetypen:
%Vor% Hier ist read eine Funktion vom Typ Read a => String -> a , was bedeutet "für jeden Typ a , der die Typklasse Read unterstützt, kann die Funktion read einen String übernehmen und einen a zurückgeben Wenn also f eine Methode ist, die einen int akzeptiert, kann ich f (read "123") schreiben und es wird "123" in Int 123 umwandeln und f damit aufrufen. Es weiß, dass es die Zeichenkette in Int umwandeln soll Weil f eine Int benötigt Wenn f eine Liste von Ints nimmt, würde es stattdessen versuchen, die Zeichenkette in eine Liste von Ints zu konvertieren. Kein Problem.
Aber für die obige Funktion readAndPrint funktioniert dieser Ansatz nicht. Das Problem hierbei ist, dass print ein Argument eines beliebigen Typs annehmen kann, der gedruckt werden kann (also jeden Typ, der die Show typeclass unterstützt). Es gibt also keine Möglichkeit für den Compiler zu wissen, ob Sie die Zeichenkette in ein int oder eine Liste von Ints oder irgendetwas anderes, das gedruckt werden kann, konvertieren wollen. In solchen Fällen müssen Sie Typ Anmerkungen hinzufügen.
In OCaml ist das problematische Feature polymorphe Funktionen in Klassen: Wenn Sie eine Funktion definieren, die ein Objekt als Argument akzeptiert und eine Methode für dieses Objekt aufruft, wird der Compiler einen monomorphen Typ für diese Methode ableiten. Zum Beispiel:
%Vor% Hier wird der Compiler folgern, dass obj eine Instanz einer Klasse sein muss, die eine Methode namens meth vom Typ int -> int hat, d. h. eine Methode, die ein Int akzeptiert und ein Int zurückgibt. Sie können nun eine Reihe von Klassen mit einer solchen Methode definieren und Instanzen dieser Klasse als Argumente an f übergeben. Kein Problem.
Das Problem tritt auf, wenn Sie eine Klasse mit einer Methode vom Typ 'a. 'a -> int definieren, d. h. eine Methode, die ein Argument eines beliebigen Typs annehmen und ein int zurückgeben kann. Sie können ein Objekt dieser Klasse nicht als Argument an f übergeben, da es nicht mit dem abgeleiteten Typ übereinstimmt. Wenn f ein solches Objekt als sein Argument verwenden soll, besteht die einzige Möglichkeit darin, eine Typ-Annotation zu f hinzuzufügen.
Das waren also Beispiele für Sprachen, die fast vollständig vom Typ abgeleitet sind, und für Fälle, in denen dies nicht der Fall ist. Wenn Sie die problematischen Funktionen aus diesen Sprachen entfernen, werden sie vollständig typabgeleitet.
Folglich sind grundlegende Dialekte von ML ohne solche erweiterten Merkmale vollständig typabgeleitet. Zum Beispiel nehme ich an, dass Caml Light vollständig vom Typ abgeleitet ist, da es im Grunde OCaml ohne Klassen ist (allerdings kenne ich die Sprache nicht, also ist das nur eine Annahme).
Was ist Typinferenz?
In der Vergangenheit führte Typ-Inferenz (oder Typ-Rekonstruktion) dazu, dass alle Typen in einem Programm abgeleitet werden können, ohne dass im Wesentlichen irgendwelche explizite Typ-Annotationen erforderlich sind. In den letzten Jahren ist es jedoch in der Programmiersprache Hauptströmung in Mode gekommen, selbst die trivialsten Formen der Bottom-up-Typableitung als "Typinferenz" zu kennzeichnen (z. B. die neuen auto Deklarationen von C ++ 11). Also haben die Leute begonnen, "voll" hinzuzufügen, um sich auf das "echte" Ding zu beziehen.
Was ist voller Inferenz?
Es gibt ein breites Spektrum, bis zu welchem Grad eine Sprache auf Typen schließen kann, und in der Praxis unterstützt fast keine Sprache eine "vollständige" Typinferenz im strengsten Sinne (Core ML ist das einzige Beispiel). Aber der Hauptunterscheidungsfaktor ist, ob Typen für Bindungen abgeleitet werden können, denen keine "Definition" zugeordnet ist - insbesondere Parameter von Funktionen. Wenn Sie schreiben können, sagen Sie
%Vor%und das Typsystem ermittelt, dass z. Hat Int → Int, dann ist es sinnvoll, diese Art Inferenz aufzurufen. Darüber hinaus sprechen wir über polymorphe Typ-Inferenz, wenn z. B.
%Vor%erhält automatisch den generischen Typ ∀ (t) t → t.
Typ-Inferenz wurde im Zusammenhang mit dem einfach-typisierten Lambda-Kalkül erfunden, und polymorphe Typ-Inferenz (auch Hindley / Milner-Typ-Inferenz, erfunden in den 1970er Jahren) ist der Anspruch auf Ruhm der ML-Familie von Sprachen (Standard ML, OCaml und wohl Haskell).
Was sind die Grenzen der vollständigen Inferenz?
Core ML hat den Luxus einer "vollständigen" polymorphen Typinferenz. Aber es hängt von bestimmten Einschränkungen des Polymorphismus in seinem Typsystem ab. Insbesondere können nur Definitionen generische und keine Funktionsargumente sein. Das heißt,
%Vor% funktioniert gut, weil id einen polymorphen Typ erhalten kann, wenn die Definition bekannt ist. Aber
tippt ML nicht ein, weil id nicht polymorph als Funktionsargument sein kann. Mit anderen Worten, das Typsystem erlaubt polymorphe Typen wie ∀ (t) t → t, aber nicht sogenannte höherrangige polymorphe Typen wie (∀ (t) t → t) → Bool, wo polymorphe Werte in a verwendet werden First-Class-Art (die, um es klar zu sagen, sogar sehr wenige explizit typisierte Sprachen erlauben).
Der polymorphe Lambda-Kalkül (auch "System F" genannt), der explizit typisiert wird, erlaubt Letzteres. Aber es ist ein Standardergebnis in der Typentheorie, dass die Typrekonstruktion für das volle System F unentscheidbar ist. Hindley / Milner trifft einen Sweetspot eines etwas weniger expressiven Typensystems, für das die Typrekonstruktion noch entscheidbar ist.
Es gibt erweiterte Systemfunktionen, die die vollständige Rekonstruktion auch unentscheidbar machen. Und es gibt andere, die es entscheidbar halten, es aber immer noch undurchführbar machen, z. das Vorhandensein von Ad-hoc-Überladung oder Subtyping, weil dies zu einer kombinatorischen Explosion führt.
Eine weitere Einschränkung sind höher eingestufte Typen. Beispielsweise überprüft das folgende Programm nicht in Sprachen mit ML-Stil-Typ-Schlussfolgerung:
%Vor%Der Typprüfungstyp kann dem Typ [Char] - & gt; [Char] oder [Int] - & gt; [Int], aber nicht für alle. [A] - & gt; [a]. In ML, Ocaml und F # gibt es keine Möglichkeit, dies zu beheben, da Sie nicht einmal höhere Rank-Typen schreiben können.
Aber Haskell (über eine GHC-Erweiterung) und Frege unterstützen höhere Rank-Typen. Da jedoch nur eine Überprüfung des Typs mit einem höheren Rang (im Gegensatz zu einer Inferenz mit einem höheren Rang) möglich ist, muss der Programmierer eine Typ-Anmerkung eingeben, beispielsweise:
%Vor%Tags und Links programming-languages functional-programming types type-inference type-systems