20
Wo liegen die Grenzen der Typinferenz? Welche Typsysteme haben keinen allgemeinen Inferenzalgorithmus?Wo liegen die Grenzen der Typinferenz?
A
Antwort
11
Joe Wells zeigte, dass Typinferenz für System F unentscheidbar ist, die die grundlegendste polymorphe Lambda-Kalkül ist, unabhängig entdeckt von Girard und Reynolds . Dies ist das wichtigste Ergebnis, das die Grenzen der Typinferenz zeigt.
Hier ist ein wichtiges Problem, das immer noch offen ist: Was ist der beste Weg, um generalisierte algebraische Datentypen in Hindley-Milner-Typ-Inferenz zu integrieren? Jedes Jahr kommt Simon Peyton Jones mit neuen Antworten auf, die angeblich besser sind als die Antwort des Vorjahres. Ich habe die Version vom März 2009 nicht gelesen und kann daher nicht sagen, ob ich davon überzeugt bin, dass sie endgültig sein wird.
5
Ein System vom Wert-abhängigen Typ (Oder kurz gesagt, System vom Typ Abhängig) kann Typen beschreiben, die sagen: "Zur Evaluierungszeit (Laufzeit) ist der Wert dieser Variablen immer gleich dem Wert davon Variable, die mit einem anderen Auswertungsprozess berechnet wird ". Die automatische Ableitung dieses Typs aus dem Code führt zu automatischen Beweisen von Theoremen. Wenn die Menge der Sätze, die Sie ausdrücken können, auf diejenigen beschränkt ist, die automatisch nachweisbar sind, wäre das kein Problem, aber im Fall von abhängig typisierten Sprachen ist dies im Allgemeinen nicht der Fall.
So abhängige typisierte Systeme können keine allgemeine (und vollständige) Inferenz haben.
Ich bin sicher, dass jemand eine moralische formale und vollständige Antwort geben kann ...
Verwandte Themen
- 1. In einem Bug/Bug-Statusmodell, wo würde der Fremdschlüssel liegen?
- 2. EC2 und EBS wie und wo liegen die Unterschiede?
- 3. Teil Typinferenz
- 4. Aufruf der Vorlagenfunktion ohne <>; Typinferenz
- 5. Wo sind die Grenzen von asp.net Dynamic Data?
- 6. Swift ObjectMapper Typinferenz
- 7. Scala Typinferenz Frage
- 8. Allgemeine Methoden Typinferenz
- 9. Was sind die Grenzen oder Bereichsdefinitionen der HTML5-Entwicklung?
- 10. Warum wird in Java 7 der Diamantoperator für Typinferenz verwendet?
- 11. Haskell lesen Typinferenz
- 12. C# Methodengruppe Typinferenz
- 13. Typinferenz mit rvalue initializer_list
- 14. scala Typinferenz mit _ Platzhalter
- 15. Sollten Sie Validierungsprüfungen durchführen, die außerhalb der normalen Benutzeraktivität liegen?
- 16. Erhalte Aufgaben, die zwischen dem Datumsbereich liegen oder außerhalb des Datumsbereichs liegen
- 17. Slick-Karussell-Folien, die übereinander liegen
- 18. Die Grenzen der Parallelität (Job Interview Frage)
- 19. Gibt es Tools oder gute Techniken, um herauszufinden, wo die Leistungsengpässe in einer iPhone-Anwendung liegen?
- 20. Wo sollte in diesem Szenario die Verantwortung für das Parsen des Eingabedatenstroms liegen?
- 21. Wo liegen meine Dateien aus der Quellcodeverwaltung unter Linux für TeamCity?
- 22. (Num a) vs Integer Typinferenz
- 23. C# 3.0 Func/SortiertNach Typinferenz
- 24. Wann Typinferenz in Haskell ausnutzen?
- 25. Warum berücksichtigt die Java 8-Typinferenz keine Ausnahmen, die von Lambdas bei der Überladungsauswahl ausgelöst werden?
- 26. Grenzen der Integration
- 27. Unexpected Typinferenz Fehler in Rust
- 28. Grenzen der Wikipedia API
- 29. Array außerhalb der Grenzen Ausnahme
- 30. ML Typinferenz auf einen C++ Programmierer
Also deckt Algorithmus W die größtmögliche Teilmenge von System F ab, die entscheidbar ist? –
@ott: Ich bin kein Spitzentheoretiker, aber ich wette mein | - Symbol, dass System F mehrere, unvergleichbare entscheidbare Untermengen hat. Ganz zu schweigen von der Möglichkeit von Erweiterungen (GADTs, Gleichheitsbeschränkungen, qualifizierte Typen). Es ist Vollbeschäftigung für die spitzköpfige Menge :-) –
@Norman Ramsey: Interessant. Ich weiß nicht, ob Typtheoretiker spitzköpfig sind, aber die Papiere, die ich gesehen habe, scheinen wirklich weit von der Realität entfernt zu sein, und ich weiß nicht, ob die Typentheorie zum Mainstream wird und allgemein akzeptiert wird; Du musst ML noch lernen, um die Grundlagen zu verstehen. –