En Conceptos en lenguajes de programación , John Mitchell escribe que la verificación de tipos estáticos es necesariamente conservadora (demasiado estricta) debido al problema de detención. Él da como ejemplo:

if (complicated-expression-that-could-run-forever)
   then (expression-with-type-error)
   else (expression-with-type-error)

¿Alguien puede proporcionar una respuesta no artificial que realmente sería una preocupación práctica?

Entiendo que Java permite conversiones verificadas dinámicamente para casos como este:

if (foo instanceof Person) {
    Person p = (Person) foo;
    :
}

pero considero que la necesidad de eso es más una deficiencia de lenguaje / compilador de Java que un problema de lenguaje cruzado.

Siempre lo he visto más como una cuestión de conveniencia, que sobre si un algoritmo puede o no expresarse en absoluto. Si realmente quisiera ejecutar programas como el de Mitchell, simplemente escribiría el simulador de máquina de Turing apropiado en mi lenguaje estáticamente escrito.

El truco con un sistema de tipo estático es ofrecer los tipos correctos de flexibilidad solo para los casos en que la flexibilidad le permite escribir código que sea más fácil de mantener.

Aquí hay algunos ejemplos de técnicas de estructuración de programas que a veces se consideran más fáciles de administrar en lenguajes dinámicos que estáticamente escritos.

Genéricos y Contenedores

En lenguajes estáticamente escritos antes de ML (c. 1973) y CLU (c. 1974) no fue difícil crear un árbol de cuerdas rojo-negro, un árbol de enteros rojo-negro, un árbol de flotadores rojo-negro, o un árbol rojo-negro de elementos de tipo específico Foo. Sin embargo, fue difícil (tal vez imposible) crear una implementación única de un árbol rojo-negro que se verificara estáticamente y que pudiera manejar cualquiera de estos tipos de datos. Las formas de solucionar el problema fueron (1) salir completamente del sistema de tipos (por ejemplo: mediante el uso devoid * en C), (2) para escribir usted mismo algún tipo de preprocesador de macros y luego escribir macros que producen el código para cada tipo específico que desee o (3) usar el enfoque Lisp / Smalltalk (y Java) para verificar el tipo de extraído Objeto dinámico.

ML y CLU introdujeron la noción de, respectivamente, tipos parametrizados inferidos y declarados explícitamente (estáticos), que le permiten escribir tipos de contenedor genéricos, de tipo estático.

Subtipo de polimorfismo

En lenguajes tipados estáticamente antes de Simula67 (c. 1967) y Hope (c. 1977) no fue posible realizar un despacho dinámico y verificar estáticamente que había cubierto el caso para cada subtipo. Muchos lenguajes tenían algún tipo de uniones etiquetados , pero fue la responsabilidad del programador para asegurarse de que sus caseo switchdeclaraciones, o sus tablas de salto, cubiertos cada etiqueta sea posible.

Los lenguajes que siguen el modelo Simula (C ++, Java, C #, Eiffel) proporcionan clases abstractas con subclases donde el compilador puede verificar que cada subclase haya implementado todos los métodos declarados por la clase padre. Los idiomas que siguen el modelo Hope (todas las variantes de ML, desde SML / NJ hasta Haskell) tienen subtipos algebraicos donde el compilador puede verificar que cada typecasedeclaración cubra todos los subtipos.

Parches de mono y programación orientada a aspectos

Los sistemas de tipo dinámico hacen que una variedad de técnicas de creación de prototipos sea mucho más fácil. En los lenguajes donde los tipos están representados por mapas hash de cadenas a funciones (por ejemplo, Python, Javascript, Ruby) es bastante fácil cambiar globalmente el comportamiento de cada módulo que se basa en un tipo particular, simplemente modificando dinámicamente el mapa hash que representa ese tipo.

Si bien hay formas obvias en que los parches de mono se pueden usar para hacer que los programas sean más difíciles de mantener, también hay formas en que realmente se pueden usar para "bien" en lugar de "mal". En particular, con la programación orientada a aspectos, uno puede usar técnicas similares a parches de mono para hacer cosas como modificar el tipo de archivo para apuntar a un sistema de archivos virtualizado, lo que permite la construcción de infraestructuras de prueba unitaria "gratis", o modificar tipos de excepción simples para que imprime mensajes de registro cada vez que son capturados para una mejor depuración.

A diferencia de Generics y Subtype Polymorphism, donde las ideas clave de verificación estática estaban disponibles en la década de 1970, la verificación estática para la programación orientada a aspectos es (creo) un área de investigación activa. No sé mucho al respecto, excepto que hay un lenguaje llamado AspectJ desde aproximadamente 2001.