Scala usa un sistema de tipos basado en el Sistema F ω, que normalmente se dice que se está normalizando fuertemente. La fuerte normalización implica la completitud no-Turing.¿Qué propiedad del sistema de tipos de Scala hace que sea Turing-complete?
Sin embargo, el sistema de tipos de Scala es Turing-completo.
¿Qué cambios/adiciones/modificaciones hacen que el sistema de tipos Scala sea completo en comparación con los algoritmos y sistemas formales?
No es una respuesta exhaustiva, pero la razón es que puede definir recursivos tipos.
He hecho preguntas similares antes (about what a non-Turing complete language might look like). Las respuestas eran de la forma: un idioma completo de Turing debe admitir el bucle arbitrario o la recursión. El sistema de tipo de Scala admite el último
recursivo existen tipos en la mayoría de los lenguajes, incluidos Java y Pascal. Cualquier tipo que se refiera a sí mismo (como una lista vinculada) es recursivo. Necesita una forma de realizar cálculos en el nivel de tipo, como tipo de aplicación. En Scala, tiene miembros de tipo y aplicación de tipo parcial en alias de tipo. –
Quise decir tipos recursivos en el sentido de la codificación peano: http://apocalisp.wordpress.com/2010/06/08/type-level-programming-in-scala/ usando 'tipo', no' clase' o ' rasgo'. Pensé que era bastante obvio dado el contexto. Como dije, me hago eco aquí, de lo que me han dicho sobre la completitud. –
[Tipos recursivos] (http://en.wikipedia.org/wiki/Recursive_data_type) se pueden usar para codificar números como usted dice, pero no son suficientes para completar Turing. Lo que quiere es una forma de calcular, en este caso usando la aplicación de tipo (que a su vez usa la sustitución). Los miembros del tipo de Scala hacen que sea algo fácil, aunque Java realiza sustituciones similares para los genéricos. –
¿Tiene enlaces/referencias? (Para los espectadores, como yo :-) –
El hecho de que el Sistema F esté fuertemente normalizado implica que el Sistema F no está completo. No implica que su sistema de tipos no lo sea. Y, de hecho, se ha demostrado que [la verificación de tipo de un Sistema F no restringido es indecidible] (http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.6.6483) – sepp2k
@ sepp2k - yikes, the Lo peor de la completitud de Turing y eso es todo. – Malvolio