20
¿Cuáles son los límites de la inferencia de tipo? ¿Qué tipo de sistema no tiene algoritmo de inferencia general?¿Cuáles son los límites de la inferencia de tipo?
A
Respuesta
11
Joe Wells mostraron que la inferencia de tipos es indecidible para el sistema de F, que es el cálculo lambda polimórfica más básico, descubierto independientemente por Girard y Reynolds . Este es el resultado más importante que muestra los límites de la inferencia de tipo.
Aquí hay un problema importante que aún está abierto: ¿cuál es la mejor manera de integrar tipos de datos algebraicos generalizados en la inferencia de tipo Hindley-Milner? Cada año, Simon Peyton Jones presenta nuevas respuestas, que supuestamente es mejor que la respuesta del año anterior. No he leído la versión de marzo de 2009 y, por lo tanto, no puedo decir si creo que será definitiva.
5
Un sistema de tipo dependiente del valor (o en resumen, sistema de tipo dependiente) puede describir los tipos que dicen cosas como: "En tiempo de evaluación (tiempo de ejecución), el valor de esta variable siempre será igual al valor variable, que se calcula con un proceso de evaluación diferente ". La deducción automática de este tipo del código implica pruebas automáticas de teoremas. Si el conjunto de teoremas que puede expresar está restringido a aquellos demostrables automáticamente, eso no sería un problema, pero en el caso de los idiomas de tipo dependiente, generalmente este no es el caso.
Así que los sistemas de tipos dependientes no pueden tener una inferencia de tipo general (y completa).
Estoy seguro de que alguien puede dar una respuesta formal y completa moral ...
Cuestiones relacionadas
- 1. ¿Cuáles son los límites de TDD?
- 2. SQLite: ¿cuáles son los límites prácticos?
- 3. ¿Cuáles son los límites de ruby en los rieles?
- 4. Almacenamiento interno de Android: ¿cuáles son los límites?
- 5. ¿Cuáles son los límites técnicos de phoneGap/Cordova?
- 6. ¿Cuáles son los límites de compilar dardos para javascript?
- 7. ¿Cuáles son las diferencias entre la inferencia tipo de Scala y C++ 11?
- 8. ¿Cuáles son algunas ventajas y desventajas de la inferencia tipo en C#?
- 9. ¿Cuáles son los límites de los sistemas de tipografía y verificación?
- 10. ¿Cuáles son los límites de usar sockets para la comunicación entre procesos?
- 11. ¿Cuáles son los límites de rendimiento teóricos en los servidores web?
- 12. ¿Cuáles son los nuevos calificadores de tipo introducidos con ARC?
- 13. ¿Cuáles son los límites de ruta de acceso de archivos de Visual Studio?
- 14. ¿Cuándo la inferencia de tipo Java produce un tipo infinito?
- 15. ¿Cuáles son los límites o las definiciones de alcance del desarrollo de HTML5?
- 16. ¿Cuáles son los límites de las funciones multi curl de PHP?
- 17. Inferencia de tipo GHC infortunios
- 18. tipo parcial inferencia
- 19. Problema de tipo Scala (inferencia)?
- 20. Sobrecarga, inferencia de tipo genérico y la palabra clave 'params'
- 21. ¿Cuáles son los límites de archivos en Git (número y tamaño)?
- 22. ¿Cuáles son los límites útiles de Autómatas limitados lineales en comparación con las Máquinas Turing?
- 23. UIView. ¿Cuáles son las dimensiones máximas de los límites que puedo usar?
- 24. ¿Cuáles son los verdaderos beneficios de ExpandoObject?
- 25. ¿Cuáles son los límites de recursión js para Firefox, Chrome, Safari, IE, etc.?
- 26. ¿Qué límites tiene Scala en la "complejidad aceptable" de los tipos inferidos?
- 27. ¿Los límites mínimos/mínimos son mínimos?
- 28. ¿Cuáles son los peligros de usar sql_variant?
- 29. ¿Cuáles son los otros valores de NaN?
- 30. ¿Cuáles son los usos de svn copy?
Entonces, ¿el algoritmo W cubre el mayor subconjunto posible del Sistema F que es decidible? –
@ott: No soy un teórico de tipo con la cabeza puntiaguda, pero apostaría mi | símbolo de que el Sistema F tiene múltiples subconjuntos decidibles incomparables. Sin mencionar la posibilidad de extensiones (GADTs, restricciones de igualdad, tipos calificados). Es el pleno empleo para la multitud de cabeza puntiaguda :-) –
@Norman Ramsey: Interesante. No sé si los teóricos del tipo son puntiagudos, pero los documentos que vi parecen estar muy lejos de la realidad y no sé si la teoría de tipos se volverá general y ampliamente aceptada; usted todavía tiene que aprender ML para incluso entender lo básico. –