¿Cuáles son los límites de los sistemas de tipografía y verificación?

Question

Los sistemas de tipo a menudo son criticados, por ser restrictivos, lo que limita los lenguajes de programación y prohíbe a los programadores escribir programas interesantes.

Chris Smith claims:

Tenemos la seguridad de que el programa es correcto (en las propiedades controladas por este tipo corrector), pero a su vez hay que rechazar algunos programas interesantes.

y

Por otra parte, hay una prueba matemática férreo que un tipo corrector de cualquier interés en absoluto es siempre conservador. Construir un verificador de tipos que no rechace ningún programa correcto no es solo difícil; es imposible.

¿Podría alguien describir qué tipo de programas tan interesantes podría ser este? ¿Dónde está probado que las fichas de tipo tienen que ser conservadoras?

Y más en general: ¿Cuáles son los límites de los sistemas de tipografía y verificación?

Answer 1

Las personas han descubierto que si primero escribe sus pruebas de una manera verdaderamente TDD, sus pruebas normalmente hacen un mejor trabajo para verificar la corrección de lo que haría un sistema estricto de verificación de tipos. Entonces, para medir la corrección, un sistema de tipo fuerte realmente no está a la altura.

El tipado fuerte a menudo puede comprar algo de velocidad porque los compiladores pueden usar fácilmente tipos nativos en lugar de tener que hacer comprobaciones de tipo en el tiempo de ejecución. Caso en cuestión: si estás haciendo un montón de matemáticas enteras, encontrarás que una implementación fuertemente tipada probablemente superará a una débilmente tipada, ya que normalmente las cifras solo pueden ser utilizadas inmediatamente por la CPU y no tendrán que ser verificado en tiempo de ejecución.

programas "Interesantes"? Por supuesto. Es más fácil escribir extensiones de un lenguaje dinámico. Además, en los 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 una interfaz 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, puedes usar esos tipos anónimos como si fueran objetos de primera clase y no tener que pasar por el dolor de codificar todos tus contratos de datos de forma explícita.

Answer 2

Puede expresar todo en un lenguaje estático y dinámico. Prueba == puedes escribir cualquier compilador de idioma en cualquier idioma completo. Entonces, sea cual sea el idioma, puede crear el lenguaje estático que hace X.

¿Qué puede ser interesante en el tipado dinámico? ... Con tipado suficientemente bueno podría interactuar con objetos a través de la red sin conocer 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á alargando las cosas un poco (¿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.

Answer 3

Es difícil encontrar comparaciones pragmáticas objetivas de los problemas de tipeo estático frente a los dinámicos, porque a menudo es una guerra tan religiosa. Los pequeños borrones de resumen que ha citado tienden a ser la misma cláusula de exención estándar que cualquiera hace que parezca "aceptable" para todos estos días.

Como alguien que tiene experiencia principalmente en idiomas estáticos, intenté comprender algunas de las concesiones en una serie de blogs hace un tiempo. Muchas advertencias, pero puede consultar la segunda mitad de this blog entry para obtener alguna 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 de la actual debate entre tipos estáticos y dinámicos. El programador puede crear tipos estáticos específicos de dominio a estructura del programa, transmitir la intención, y descartar una clase de errores y comportamientos en tiempo de compilación, al precio de tener al autor que estructura y mediar estructural desajustes en los límites del módulo. O el programador puede optar por calcular más todo con sólo escalares y listas, en el que los datos de casos fluye fácilmente en todas partes, lo que resulta en código corto, pero con la pérdida de tiempo de compilación cheques y conducción de la intención.

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.

Answer 4

Creo que an eval function puede ser útil a veces, pero nunca es necesario (no es común para un lenguaje estáticamente tipado, consulte la explicación en el enlace).

Answer 5

Aquí está un ejemplo sencillo (en Python, pero nada que ver 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 prever cualquier tipo de posibles excepciones a las normas, especialmente si estás creando un marco base que será utilizado por las personas mucho más tarde.

Para responder a su pregunta directa, ¿de qué lado está usted en: Programador A o Programador B?

Answer 6

Un ejemplo interesante es This Paper, que es probablemente la única comparación de manzanas a manzanas que se haya realizado nunca en la tipificación estática frente a la dinámica. Implementaron self (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 tipo tuvo muchos problemas para resolver entre enteros de máquina y enteros de precisión arbitrarios. Se auto-promocionaron en vainilla y, por lo tanto, el sistema de tipos no lo diferenciaba. significaba que el compilador debía incluir código para promocionar a BigInt en cada operación de entero.

Corrieron en contra de un límite de su sistema de tipo: No podía examinar el valor real de los enteros.

Creo que no existen límites teóricos para el tipo de sistemas en general, pero cualquier comprobador de tipos determinado solo puede tratar con un sistema específico de tipo limitado, y habrá programas en los que no se puede determinar lo que está sucediendo. Como el inferencer de tipo propio permitía conjuntos de tipos, simplemente compilaba ambas rutas. Un verificador de tipos que requiera convergencia en un solo tipo debería rechazar el programa. (Aunque probablemente tenga un código especial para este caso.)

Answer 7

No estoy seguro, pero creo que los problemas a los que se refiere son sistemas de tipo algebraico como Haskell y ML. Estos lenguajes intentan hacer un análisis "estático" muy completo de los tipos incluso antes de ejecutar 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 distintos tipos.

Por ejemplo, en la mayoría de los lenguajes 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 estricta que tendría que hacer un tipo unificado de envolver y luego el ajuste de patrones 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 potente meta-programación y enlace de datos que no puede hacer con un análisis estático completo.

Answer 8

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 take int como parámetro; abs siempre devuelve int, pero signum puede devolver int o cadena. Ahora, si presentamos un verificador de tipos (pero no cualquier verificador de tipos; el verificador de tipos de Scala diría "signum es int->Any"!) Este programa sería rechazado ... aún así, es correcto y nunca se bloqueará con el no- la conformidad de tipo fuerte como la razón del accidente.

Answer 9

SpeC# tiene un sistema tipo con tipos no nulos y es estáticamente seguro. (http://research.microsoft.com/en-us/projects/specsharp/)

Answer 10

¿Cuáles son los límites de los sistemas de tipografía y tipo?

Voy a suponer que "sistemas tipo" implica un lenguaje de programación tipado estáticamente.

tipado estático significa que los tipos se comprueban en tiempo de compilación. La limitación aquí es que el compilador solo puede optimizar en función de la información disponible en el momento de la compilación. Esto podría considerarse una limitación. En lenguajes de programación de tipo dinámico, el intérprete podría analizar y optimizar el programa en tiempo de ejecución. Esto significa que puede optimizar en función de los patrones de uso.

Answer 11

Creo que la primera declaración es técnicamente incorrecta, aunque correcta en la práctica.

La tipificación estática es esencialmente lo mismo que probar las propiedades de los programas, y al usar una lógica lo suficientemente poderosa, podría probar que todos los programas interesantes son correctos.

El problema es que, para las poderosas lógicas, 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 proponentes de orden superior 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 verificación de tipo para esa entrada.

En cuanto a la segunda declaración, puede estar refiriéndose al teorema de incompletitud de Gödels. Establece que para cualquier sistema de prueba dado hay afirmaciones verdaderas de aritmética (la lógica de adición y multiplicación de números naturales) que no pueden ser probadas en el sistema de prueba. Traducido a sistemas de tipo estático tendrías un programa que no hace nada malo, pero el sistema de tipo estático no podría probar eso.

Estos contraejemplos se construyen refiriéndose a la definición del sistema de prueba, diciendo esencialmente "No se puede probar" traducido a aritmética, lo que no es muy interesante. En mi humilde opinión, un programa construido análogamente tampoco sería interesante.

Answer 12

Si mira Mitchell's book Concepts in Programming Languages p.134, encontrará algunos detalles sobre lo que se denomina la "Conservatividad de la comprobación de tiempo de compilación". El problema es que algunas características "interesantes", como los accesos fuera de límites para las matrices, no se pueden verificar estáticamente, ya que requerirían una evaluación del programa/cada ejecución de programa posible. El resultado estándar de indecidibilidad le dice que tendría que resolver el problema de Detención para verificar de hecho CADA acceso a la matriz.

Answer 13

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 lenguaje completo de Turing puede hacer lo mismo que cualquier otro, por lo que es falso que haya algunos programas en lenguajes tipados dinámicamente que no se pueden reproducir, por ejemplo, en Haskell.

El problema es que el hecho de que un sistema de tipo rechace un programa no significa que rechazará todos los programas equivalentes a él. Por lo tanto, algunos programas serán rechazados, pero puede reemplazarlos por otros programas equivalentes. Como un ejemplo, el siguiente programa de Scala

def foo: Int = 
    if (1 > 0) 15 else "never happens" 

El tipo de corrector lo rechazará, como la expresión if (1 > 0) 15 else "never happens" es formalmente de tipo Any. Cuando lo ejecute, sin duda devolverá un número entero, pero sin evaluar 1 > 0 no puede estar seguro de que no devolverá una cadena. Puede 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, existen programas equivalentes a ésta que se puede escribir en Scala, siendo el más simple

def foo: Int = 15