types - uhf - ¿Cuáles son los límites de verificación de tipos y sistemas de tipos?
tipos de tags (13)
¿Cuáles son los límites de verificación de tipos y sistemas de tipos?
Voy a suponer que "sistemas de tipo" implica un lenguaje de programación estático.
La escritura estática significa que los tipos se verifican en el momento de la compilación. La limitación aquí es que el compilador solo puede optimizar en función de la información que está disponible en el momento de la compilación. Esto podría considerarse una limitación. En los lenguajes de programación tipificados dinámicamente, el intérprete podría analizar y optimizar el programa en tiempo de ejecución. Esto significa que puede optimizar basado en patrones de uso.
Los sistemas de tipos a menudo son criticados, por ser demasiado restrictivos, es decir, limitar los lenguajes de programación y prohibir que los programadores escriban programas interesantes.
Chris Smith claims :
Tenemos la seguridad de que el programa es correcto (en las propiedades verificadas por este comprobador de tipos), pero a su vez debemos rechazar algunos programas interesantes.
y
Además, existe una prueba matemática irrefutable de que un verificador de tipo de cualquier interés es siempre conservador. Crear un comprobador de tipos que no rechace los programas correctos no solo es difícil; es imposible.
¿Podría alguien por favor describir qué tipo de programas interesantes podría ser? ¿Dónde está comprobado que los controladores de tipos tienen que ser conservadores?
Y más general: ¿Cuáles son los límites de la verificación de tipos y los sistemas de tipos?
Aquí hay un ejemplo simple (en Python, pero no relacionado con sus problemas de escritura):
# The company deals with rectangles. They have horizontal and vertical lengths
# that should not be mixed. Programmer A writes:
class Rectange:
def __init__(self, width, height):
enforce_type(''horizontal'', width)
enforce_type(''vertical'', height)
#
# A: Hehe! I''m so smart! With my patented type system if I try to
# write "width * width" I''ll have a loud error so I''ll know I''m wrong.
#
area = width * height
enforce_type(''square_meters'', area)
...
# Everyone''s happy. The company shows off A''s type system on the conference.
...
# Much later, the clients request ability to specify square by entering only
# one length. Programmer B writes:
class Square(Rectangle):
def __init__(self, width):
Rectange.__init__(self, width, width)
# !!
# Error happens! ''horizontal'' is not ''vertical''!
#
# B: Dear Management, I would like to request a weeklong leave since I
# have to track Programmer A''s house and either talk him into changing
# his patented type system or BEAT HIM WITH MY LAPTOP until he agrees.
#
Es muy difícil crear un sistema de tipos que prevea cualquier tipo de posibles excepciones a las reglas, especialmente si está creando un marco base que será utilizado por las personas mucho más tarde.
Para responder a su pregunta directa, ¿de qué lado está: Programador A o Programador B?
Creo que una función eval podría ser útil a veces, pero nunca es necesaria (no es común en un lenguaje de tipo estático, consulte la explicación en el enlace).
Creo que hay un malentendido. Es cierto que cualquier sistema de tipo rechazará un programa correcto (no recuerdo el nombre exacto del resultado, por lo que no puedo buscarlo ahora, lo siento). Al mismo tiempo, es cierto que cualquier idioma completo de Turing puede hacer lo mismo que cualquier otro, por lo que es falso que haya algunos programas en idiomas tipificados dinámicamente que no puede reproducir, por ejemplo, en Haskell.
El problema es que el hecho de que un sistema de tipos rechace un programa no significa que rechazará todos los programas equivalentes a él. Así que algunos programas serán rechazados, pero puede reemplazarlos con otros programas equivalentes. Como ejemplo, tome el siguiente programa Scala
def foo: Int =
if (1 > 0) 15 else "never happens"
El comprobador de tipos lo rechazará, ya que la expresión if (1 > 0) 15 else "never happens" es formalmente de tipo Any . Cuando lo ejecute, sin duda devolverá un entero, pero sin evaluar 1 > 0 no puede estar seguro de que no devolverá una cadena. Podrías escribir, en Python.
def foo():
if 1 > 0:
return 15
else:
return "never happens"
y al compilador de Python no le importaría.
Por supuesto, hay programas equivalentes a este que puedes escribir en Scala, el más simple es
def foo: Int = 15
Creo que la primera afirmación es técnicamente incorrecta, aunque correcta en la práctica.
La escritura estática es esencialmente lo mismo que probar las propiedades de los programas, y al usar una lógica suficientemente poderosa, se podría probar que todos los programas interesantes son correctos.
El problema es que para la lógica, la inferencia de tipos ya no funciona, y debe proporcionar las pruebas como parte del programa para que el verificador de tipos pueda hacer su trabajo. Un ejemplo concreto son los probadores de orden superior tales como Coq. Coq usa una lógica extremadamente poderosa, pero también es extremadamente tedioso hacer algo en Coq, porque tienes que proporcionar pruebas con gran detalle.
El tipo de programas interesantes que le causarán más problemas serán los intérpretes, ya que su comportamiento depende completamente de una entrada. Esencialmente, deberá probar de manera reflexiva la corrección de la comprobación de tipo para esa entrada.
En cuanto a la segunda afirmación, puede estar refiriéndose al teorema de incompletitud de Gödels. Establece que para cualquier sistema de prueba dado hay declaraciones verdaderas de aritmética (la lógica de suma y multiplicación de números naturales) que no se pueden probar en el sistema de prueba. Traducido a sistemas de tipo estático, tendría un programa que no hace nada malo, pero el sistema de tipo estático no pudo demostrarlo.
Estos contraejemplos se construyen refiriéndose a la definición del sistema de prueba, diciendo esencialmente que "no se puede probar" traducido a aritmética, lo cual no es muy interesante. En mi humilde opinión, un programa construido de forma análoga tampoco sería interesante.
Es difícil encontrar comparaciones pragmáticas objetivas de los problemas de tipografía estática y dinámica, porque a menudo es una guerra tan religiosa. Los pequeños blubs de resumen que usted ha citado tienden a ser el mismo descargo de responsabilidad que cualquier persona hace que parece ser "aceptable" para todos en estos días.
Como alguien que tiene experiencia en su mayoría en lenguajes estáticos, traté de entender algunas de las compensaciones en una serie de blogs hace un tiempo. Hay muchas advertencias, pero puede consultar la segunda mitad de esta entrada del blog para obtener una comparación que sea sugerente como respuesta a su pregunta.
Aquí hay una cita que sugiere una ventana a las compensaciones:
En cierto sentido, esta pequeña función captura la esencia del debate en curso entre la escritura estática y la dinámica. El programador puede crear tipos estáticos específicos del dominio para estructurar el programa, transmitir la intención y descartar una clase de errores y comportamientos en tiempo de compilación, al precio de tener que crear esa estructura y mediar los desajustes estructurales en los límites del módulo. O el programador puede optar por calcular casi todo con solo escalas y listas, en cuyo caso los datos fluyen fácilmente a todas partes, lo que resulta en un código corto, pero con la pérdida de controles en tiempo de compilación y la transmisión de intenciones.
y el ejemplo en ejecución muestra un caso en el que el programa de tipo estático no permite un comportamiento útil / interesante por su naturaleza.
Hay muchos ejemplos complejos, pero parece que la mayoría de las personas se pierden el ejemplo trivial.
Este es un programa Python correcto que responde a la pregunta de cuáles son los valores absolutos de 5 y -5.
def abs(x):
def signum(f):
if f > 0:
return 1
else:
return "non-positive"
if signum(x) == 1:
return x
else:
return -x
print("abs(5) = %r and abs(-5) = %r" % (abs(5), abs(-5)))
Obviamente, abs y signum toman int como parámetro; abs siempre devuelve int, pero signum puede devolver int o string. Ahora, si introdujéramos un verificador de tipo (pero no cualquier verificador de tipo; el verificador de tipo de int->Any solo diría "signum is int->Any "!) Este programa sería rechazado ... sin embargo, es correcto y nunca se bloqueará La conformidad de tipo no fuerte como la razón de la caída.
La gente ha descubierto que si escribe sus pruebas primero de una manera verdaderamente TDD, las pruebas generalmente hacen un mejor trabajo para verificar la corrección que un sistema de verificación de tipo estricto. Por lo tanto, para medir la corrección, un sistema de tipo sólido realmente no está a la altura.
La escritura fuerte a menudo puede ofrecerle algo de velocidad porque los compiladores pueden usar fácilmente tipos nativos en lugar de tener que hacer verificaciones de tipos en tiempo de ejecución. Caso en cuestión: si está haciendo un montón de matemáticas de enteros, encontrará una implementación fuertemente tipificada que probablemente superará a una tipificada débilmente, ya que sus cifras normalmente pueden ser utilizadas inmediatamente por la CPU y no tendrán que serlo. verificado en tiempo de ejecución.
¿Programas "interesantes"? Por supuesto. Es más fácil escribir extensiones desde un lenguaje dinámico. Además, en sistemas distribuidos, puede ser realmente conveniente tener una IU de tipo débil y no tener que generar objetos de transferencia de datos específicos. Por ejemplo, si tiene un front end de JavaScript y un backend de C #, puede usar LINQ en el extremo de C # para generar clases anónimas y enviarlas a su Javascript a través de JSON. Desde la capa JS, puede usar esos tipos anónimos como si fueran objetos de primera clase y no tener que pasar por el dolor de codificar todos sus contratos de datos explícitamente.
No estoy seguro, pero creo que los problemas a los que se refiere están relacionados con los sistemas de tipo algebraico como Haskell y ML. Estos lenguajes intentan hacer un análisis "estático" muy completo de los tipos antes de que incluso ejecutes el programa.
Algunas molestias interesantes con un análisis estático muy estricto en sistemas de tipo algebraico es que es muy difícil tener un contenedor que contenga una mezcla de objetos de diferentes tipos.
Por ejemplo, en la mayoría de los idiomas principales, puede tener una mezcla heterogénea de tipos en una lista. Un ejemplo en python sería:
["a",1,"b",2]
Para hacer esto en un sistema de tipo estricto, tendría que hacer un tipo unificado de ajuste y luego ajustar el patrón a todos los tipos posibles.
Pero lo realmente interesante que falta en los idiomas es la poderosa introspección que tiene en el lenguaje más moderno (por ejemplo, C #, Java, Python, Ruby, Lisp).
En consecuencia, estos lenguajes le permiten realizar una metaprogramación poderosa y un enlace de datos que no puede hacer con un análisis estático completo.
Puedes expresar todo en lenguaje tanto estático como dinámico. Prueba == puede escribir cualquier compilador de idioma en cualquier idioma completo. Cualquiera que sea el idioma, puedes crear el lenguaje estático que hace X.
¿Qué puede ser interesante en la tipificación dinámica? ... Con una tipificación de pato suficientemente buena, podría interactuar con objetos a través de la red sin saber nunca sus tipos y pasar sus resultados (de un tipo desconocido para usted) como parámetros a las funciones locales que realmente pueden hacer. algo útil.
La respuesta estática a ese problema sería envolver todo en "interfaz exportable" proporcionando .call () y .provides? () Trabajando en el nombre del texto, pero eso sería definitivamente más difícil.
Ese es el caso más "limitante" que conozco y realmente está estirando un poco las cosas (¿solo es realmente útil con objetos simulados?). En cuanto a los límites teóricos, no hay ninguno, solo necesitas un código adicional para superar los problemas prácticos.
Si observa el libro de Mitchell Concepts in Programming Languages p.134, encontrará algunos detalles sobre lo que se denomina "Conservación de la verificación en tiempo de compilación". El problema es que algunas características "interesantes" como los accesos fuera de los límites para los arreglos no se pueden verificar de forma estática, ya que requerirían una evaluación del programa / cada posible ejecución del programa. El resultado estándar de indecidibilidad indica que tendrías que resolver el problema de la detención para verificar CADA acceso a la matriz.
Spec # tiene un sistema de tipos con tipos no nulos y es estáticamente seguro. ( http://research.microsoft.com/en-us/projects/specsharp/ )
Un ejemplo interesante es This Paper , que es probablemente la única comparación de manzanas con manzanas que se haya hecho en la escritura estática frente a la dinámica. Se implementaron (un lenguaje como smalltalk, pero con prototipos en lugar de clases) con inferencia de tipo (estática) y retroalimentación de tipo (dinámica).
El resultado más interesante es que el motor de inferencia de tipos tuvo muchos problemas para resolver entre enteros de máquina y enteros de precisión arbitrarios. Se promovieron automáticamente en el mismo tipo de vainilla y, por lo tanto, el sistema de tipos no pudo diferenciarlos, lo que significa que el compilador Tenía que incluir código para promover a BigInt en cada operación de enteros.
Se encontraron con un límite de su sistema de tipos: no podía examinar el valor real de los enteros.
Creo que no hay límites teóricos para los sistemas de tipo en general, pero cualquier comprobador de tipo dado solo puede tratar con un sistema de tipo limitado y específico, y habrá programas en los que no puede determinar qué está sucediendo. Dado que el inferencio de tipo propio permitía conjuntos de tipos, simplemente compilaba ambas rutas. Un verificador de tipos que requiera convergencia en un solo tipo tendría que rechazar el programa. (Aunque probablemente tendría un código especial para este caso).