scala - ¿Cuál es la razón de un sistema de tipo completo de Turing
haskell turing-complete (1)
¿Qué significa realmente en el contexto de los tipos?
Significa que el sistema de tipos tiene suficientes características para representar cálculos arbitrarios. Como una prueba muy breve, presento a continuación una implementación a nivel de tipo del cálculo de SK ; Hay muchos lugares que discuten la integridad de Turing de este cálculo y lo que significa, así que no repetiré eso aquí.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
infixl 1 `App`
data Term = S | K | App Term Term
type family Reduce t where
Reduce S = S
Reduce K = K
Reduce (S `App` x `App` y `App` z) = Reduce (x `App` z `App` (y `App` z))
Reduce (K `App` x `App` y) = Reduce x
Reduce (x `App` y) = Reduce (Reduce x `App` y)
Puedes ver esto en acción en un aviso de ghci; por ejemplo, en el cálculo de SK , el término SKSK reduce (eventualmente) a solo K :
> :kind! Reduce (S `App` K `App` S `App` K)
Reduce (S `App` K `App` S `App` K) :: Term
= ''K
Aquí hay una divertida para probar también:
> type I = S `App` K `App` K
> type Rep = S `App` I `App` I
> :kind! Reduce (Rep `App` Rep)
No arruinaré la diversión, pruébalo tú mismo. Pero primero saber cómo terminar programas con extremo prejuicio.
¿Podría alguien dar un ejemplo de cómo un programador puede beneficiarse de ello?
El cálculo arbitrario de nivel de tipo le permite expresar invariantes arbitrarios en sus tipos y hacer que el compilador verifique (en tiempo de compilación) que están preservados. ¿Quieres un árbol rojo-negro? ¿Qué tal un árbol rojo-negro que el compilador puede verificar conserva las invariantes rojo-negro-árbol? Eso sería útil, ¿verdad, ya que descarta toda una clase de errores de implementación? ¿Qué tal un tipo de valores XML que se sabe estáticamente que coincide con un esquema en particular? De hecho, ¿por qué no ir un paso más allá y escribir un tipo parametrizado cuyo parámetro representa un esquema? Luego, podría leer un esquema en tiempo de ejecución y hacer que sus verificaciones en tiempo de compilación garanticen que su valor parametrizado solo puede representar valores bien formados en ese esquema. ¡Bonito!
O, quizás, un ejemplo más prosaico: ¿qué pasaría si su compilador verificara que nunca indexó su diccionario con una clave que no estaba allí? Con un sistema tipográfico suficientemente avanzado, puedes.
Por supuesto, siempre hay un precio. En Haskell (y probablemente en Scala?), El precio de una prueba de compilación muy emocionante es gastar una gran cantidad de tiempo y esfuerzo del programador para convencer al compilador de que lo que está verificando es cierto, y esto a menudo es tanto alto Costo inicial así como un alto costo de mantenimiento continuo.
Esta pregunta ya tiene una respuesta aquí:
Scala y Haskell tienen "sistemas de tipo completo de Turing". Por lo general, la integridad de Turing se refiere a cálculos y lenguajes . ¿Qué significa realmente en el contexto de los tipos?
¿Podría alguien dar un ejemplo de cómo un programador puede beneficiarse de ello?
PD: no quiero comparar los sistemas tipográficos de Haskell y Scala. Es más sobre el término en general.
PSS Si es posible más ejemplos de Scala.