sintaxis programar introduccion instanciar crear clases clase language-agnostic scala type-systems turing-complete

language-agnostic - programar - scala introduccion



El sistema de tipos en Scala está completo. ¿Prueba? ¿Ejemplo? Beneficios? (2)

Existen afirmaciones de que el sistema de tipos de Scala está completo. Mis preguntas son:

  1. ¿Hay alguna prueba formal de esto?

  2. ¿Cómo se vería un simple cálculo en el sistema de tipo Scala?

  3. ¿Esto es beneficioso para Scala, el idioma? ¿Esto hace que Scala sea más "poderosa" de alguna manera en comparación con los idiomas sin un sistema de tipo Turing completo?

Supongo que esto se aplica a los idiomas y sistemas de tipo en general.

Hay una publicación de blog en algún lugar con una implementación de nivel de tipo del cálculo del combinador SKI, que se sabe que es Turing-completo.

Los sistemas de tipo Turing-completo tienen básicamente los mismos beneficios y desventajas que tienen los lenguajes completos de Turing: puede hacer cualquier cosa, pero puede probar muy poco. En particular, no puedes probar que eventualmente harás algo.

Un ejemplo de computación a nivel de tipo son los nuevos transformadores de recolección preservadores de tipo en Scala 2.8. En Scala 2.8, se garantiza que métodos como map , filter , etc. devolverán una colección del mismo tipo en el que se invocaron. Entonces, si filter un Set[Int] , obtiene un Set[Int] y si map un List[String] obtiene una List[Whatever the return type of the anonymous function is] .

Ahora, como puede ver, el map puede transformar el tipo de elemento. Entonces, ¿qué ocurre si el nuevo tipo de elemento no se puede representar con el tipo de colección original? Ejemplo: un BitSet solo puede contener enteros de ancho fijo. Entonces, ¿qué sucede si tiene un BitSet[Short] y BitSet[Short] cada número a su representación de cadena?

someBitSet map { _.toString() }

El resultado sería un BitSet[String] , pero eso es imposible. Entonces, Scala elige el BitSet más derivado de BitSet , que puede contener una String , que en este caso es un Set[String] .

Todo este cálculo se lleva a cabo durante el tiempo de compilación , o más precisamente durante el tiempo de verificación de tipo , usando funciones de tipo de nivel. Por lo tanto, está garantizado estáticamente como seguro para el tipo, aunque los tipos se calculan realmente y, por lo tanto, no se conocen en el momento del diseño.