Categorización de sistemas de tipos (fuerte / débil, dinámico / estático)

En resumen: ¿cómo se clasifican los sistemas de tipos en contextos académicos; particularmente, ¿dónde puedo encontrar fuentes confiables que aclaren las distinciones entre los diferentes tipos de sistemas de tipos?

En cierto sentido, la dificultad con esta pregunta no es que no pueda encontrar una respuesta, sino que puedo encontrar demasiadas, y ninguna se destaca como correcta. El trasfondo es que estoy tratando de mejorar un artículo en el wiki de Haskell sobre mecanografía , que actualmente afirma las siguientes distinciones:

• Sin escribir: el idioma no tiene noción de tipos, o desde una perspectiva escrita: hay exactamente un tipo en el idioma. El lenguaje ensamblador solo tiene el tipo 'patrón de bits', Rexx y Tk solo tienen el tipo 'texto', el núcleo MatLab solo tiene el tipo 'matriz de valores complejos'.
• Escritura débil: solo hay unos pocos tipos distinguidos y quizás sinónimos de varios tipos. Por ejemplo, C usa números enteros para booleanos, enteros, caracteres, conjuntos de bits y enumeraciones.
• Tipografía fuerte: conjunto de tipos de grano fino como en Ada, idiomas wirthianos (Pascal, Modula-2), Eiffel

Esto es completamente contrario a mi percepción personal, que estaba más en la línea de:

• Escritura débil: los objetos tienen tipos, pero se convierten implícitamente a otros tipos cuando el contexto lo exige. Por ejemplo, Perl, PHP y JavaScript son todos los lenguajes en los que "1"se puede usar en más o menos cualquier contexto que se 1pueda.
• Escritura fuerte: los objetos tienen tipos y no hay conversiones implícitas (aunque se puede utilizar una sobrecarga para simularlos), por lo que usar un objeto en el contexto incorrecto es un error. En Python, indexar una matriz con una cadena o flotante genera una excepción TypeError; en Haskell fallará en el momento de la compilación.

Pedí opiniones sobre esto a otras personas con más experiencia en el campo que yo, y uno dio esta caracterización:

• Escritura débil: realizar operaciones no válidas en los datos no se controla ni se rechaza, sino que simplemente produce resultados no válidos / arbitrarios.
• Escritura fuerte: las operaciones con datos solo se permiten si los datos son compatibles con la operación.

Según tengo entendido, la primera y la última caracterización llamarían a C débilmente tipado, la segunda lo llamaría fuertemente tipado. El primero y el segundo llamarían a Perl y PHP débilmente tipados, el tercero los llamaría fuertemente tipados. Los tres describirían Python como fuertemente tipado.

Creo que la mayoría de la gente me diría "bueno, no hay consenso, no hay un significado aceptado de los términos". Si esas personas están equivocadas, yo estaría feliz de oír hablar de eso, pero si están en lo cierto, entonces ¿ Cómo describo investigadores CS y comparar los sistemas de tipo? ¿Qué terminología puedo usar que sea menos problemática?

Como una pregunta relacionada, creo que la distinción dinámica / estática a menudo se da en términos de "tiempo de compilación" y "tiempo de ejecución", lo que me parece insatisfactorio dado que si un idioma se compila o no no es una propiedad de ese idioma como sus implementaciones. Siento que debería haber una descripción puramente semántica de la escritura dinámica versus la estática; algo parecido a "un lenguaje estático es aquel en el que se puede escribir cada subexpresión". Agradecería cualquier pensamiento, particularmente referencias, que aporten claridad a esta noción.

Históricamente, el término "lenguaje de programación fuertemente tipado" entró en uso en los años 70 como reacción a los lenguajes de programación existentes ampliamente utilizados, la mayoría de los cuales tenían agujeros tipográficos. Algunos ejemplos:

• En Fortran, había cosas llamadas áreas de almacenamiento "COMÚN", que podían compartirse entre los módulos, pero no hubo verificaciones para ver si cada módulo declaraba el contenido del almacenamiento COMÚN con los mismos tipos. Entonces, un módulo podría declarar que un bloque de almacenamiento COMÚN particular tenía un número entero y otro un número de coma flotante, y como resultado los datos se corromperían. Fortran también tenía declaraciones de "EQUIVALENCIA", por las cuales se podía declarar que el mismo almacenamiento contenía dos objetos diferentes de diferentes tipos.

• En Algol 60, el tipo de parámetros de procedimiento se declaró simplemente como "procedimiento", sin especificar los tipos de parámetros del procedimiento. Entonces, uno podría suponer que un parámetro de procedimiento era un procedimiento de aceptación de enteros, pero pasar un procedimiento de aceptación real como argumento. Esto daría como resultado el mismo tipo de corrupción que las declaraciones COMUNES y EQUIVALENCIA. (Sin embargo, Algol 60 eliminó los problemas más antiguos).

• En Pascal, se agregaron "registros de variantes" que eran casi exactamente como las antiguas declaraciones de EQUIVALENCIA.

• En C, se agregaron "conversiones de tipo" por las cuales cualquier tipo de datos podría reinterpretarse como datos de un tipo diferente. Este fue un agujero de tipo bastante deliberado destinado a programadores que supuestamente saben lo que están haciendo.

Los lenguajes fuertemente tipados diseñados en los años 70 estaban destinados a eliminar todos esos agujeros de tipo. Si profundiza en lo que esto significa, significa esencialmente que las representaciones de datos están protegidas. No es posible ver el objeto de datos de un tipo como un objeto de otro tipo que tiene el mismo patrón de bits que su representación interna. Los teóricos comenzaron a usar el término "independencia de representación" para caracterizar esta propiedad en lugar de la vaga idea de "mecanografía fuerte".

Tenga en cuenta que los lenguajes tipados dinámicamente como Lisp que realizan una verificación completa de tipos en tiempo de ejecución están "tipados fuertemente" en el sentido de proteger representaciones. Al mismo tiempo, los lenguajes tipados estáticamente perderían independencia de representación a menos que hicieran una verificación de los límites de la matriz. Por lo tanto, no están "fuertemente tipados" en el sentido estricto del término. Debido a estas consecuencias anómalas, el término "fuertemente tipado" quedó en desuso después de los años 70. Cuando el Departamento de Defensa de los EE. UU. Desarrolló requisitos rigurosos para el diseño de Ada, incluyeron el requisito de que el lenguaje debe ser "fuertemente tipado". (Parece que en ese momento se creía que la idea de "fuertemente tipado" era evidente. No se ofreció ninguna definición. ) Todas las propuestas de idiomas presentadas en respuesta afirmaron estar "fuertemente tipadas". Cuando Dijkstra analizó todas las propuestas de lenguaje, descubrió que ninguna de ellas estaba fuertemente tipada y, de hecho, ni siquiera estaba claro qué significaba el término. Ver el informeEWD663 . Sin embargo, veo que el término está volviendo a usarse ahora, a través de una generación más joven de investigadores que no conocen el historial a cuadros del término.

El término "tipeado estáticamente" significa que toda la verificación de tipo se realiza de forma estática y que no se producirán errores de tipo en tiempo de ejecución. Si el idioma también está fuertemente tipado, eso significa que realmente no hay errores de tipo durante la ejecución. Si, por otro lado, hay agujeros de tipo en el sistema de tipo, la ausencia de errores de tipo en tiempo de ejecución no significa nada. Los resultados podrían ser completamente corruptos.

El nuevo debate sobre "mecanografía fuerte frente a débil" parece ser acerca de si se deben permitir ciertas conversiones de tipos. Permitir una cadena donde se requiere un número entero es "escribir débilmente" según estas personas. Tiene cierto sentido porque puede fallar el intento de convertir una cadena en un entero, si la cadena no representa un entero. Sin embargo, convertir un número entero en una cadena no tiene ese problema. ¿Sería una instancia de "mecanografía débil" según estas personas? No tengo idea. Noté que las discusiones de Wikipedia sobre "mecanografía débil" no citan ninguna publicación arbitrada. No creo que sea una idea coherente.

Nota agregada : El punto básico es que el término "mecanografía fuerte" no entró en uso como un término técnico con una definición rigurosa. Se parecía más a algunos diseñadores de idiomas: "nuestro sistema de tipos es fuerte; detecta todos los errores de tipo; no tiene agujeros de tipo" y, por lo tanto, cuando publicaron su diseño de lenguaje, afirmaron que estaba "fuertemente tipeado" . Era una palabra de moda que sonaba bien y la gente comenzó a usarla. El documento de Cardelli-Wegner fue el primero que vi en el que se proporcionó un análisis de lo que significa. Mi publicación aquí debe considerarse como una elaboración de su posición.

El artículo que Uday Reddy encontró en su respuesta, Sobre tipos de comprensión, abstracción de datos y polimorfismo (1985), da las siguientes respuestas:

Se dice que los lenguajes de programación en los que el tipo de cada expresión puede determinarse mediante análisis de programa estático se tipan estáticamente. La escritura estática es una propiedad útil, pero el requisito de que todas las variables y expresiones estén vinculadas a un tipo en tiempo de compilación a veces es demasiado restrictivo. Puede ser reemplazado por el requisito más débil de que se garantiza que todas las expresiones sean de tipo coherente, aunque el tipo en sí puede ser estáticamente desconocido; Esto puede hacerse generalmente mediante la introducción de alguna verificación de tipo en tiempo de ejecución. Los idiomas en los que todas las expresiones son de tipo consistente se denominan idiomas fuertemente tipados. Si un idioma está fuertemente tipado, su compilador puede garantizar que los programas que acepta se ejecutarán sin errores de tipo. En general, debemos esforzarnos por una escritura fuerte y adoptar una escritura estática siempre que sea posible.

Se pueden encontrar respuestas autorizadas en el artículo de la encuesta de Cardelli y Wegner: Sobre los tipos de comprensión, la abstracción de datos y el polimorfismo .

Eso sí, mientras que "mecanografía fuerte" tiene un significado aceptado, "mecanografía débil" no. Cualquier falla de tipeo fuerte puede considerarse débil y las personas pueden diferir sobre qué tipo de falla es aceptable y qué no.