¿Cómo se debe leer la notación de los sistemas de tipos?

• Este artículo ofrece una explicación detallada sobre cómo leer y entender la notación de los sistemas de tipos en los lenguajes de programación.
• La notación de los sistemas de tipos es una expresión matemática usada en artículos o papers sobre sistemas de tipos.
• La notación usada para describir sistemas de tipos varía según la presentación, pero la mayoría comparte muchas partes en común.
• Un sistema de tipos aplicado a un lenguaje de programación es un sistema sintáctico: un conjunto de reglas que actúa sobre la sintaxis del lenguaje de programación.
• Esta notación se origina en la lógica formal y se usa para construir demostraciones formales sobre las propiedades de un sistema.
• El artículo también analiza los conceptos de relación, juicio, axioma y regla de inferencia dentro de la notación de sistemas de tipos.
• La relación de tipado normalmente se escribe como e:τ y puede leerse como "e tiene tipo τ".
• El juicio de tipado se escribe con la notación ⊢e:τ⊢, donde ⊢ puede leerse con el significado de "la siguiente afirmación es verdadera".
• El artículo también explica en detalle los conceptos de variable, contexto y entorno dentro de la notación de sistemas de tipos.
• El contexto o entorno de tipos se representa en la notación como Γ.
• El artículo también cubre otras notaciones y consideraciones comunes, como la disposición de las reglas de inferencia, las condiciones laterales, el subtipado, los múltiples contextos y la verificación de tipos bidireccional.
• Este artículo es una guía integral para entender la notación de los sistemas de tipos, especialmente para quienes son nuevos en este concepto.

[GN⁺]

Comentario de Hacker News

• Discusión sobre la notación de sistemas de tipos en artículos de ciencias de la computación, con una explicación básica de la notación BNF y las reglas de inferencia
• Se rastrea el origen de la notación hasta Frege, y los elementos clave son el símbolo del torniquete y la línea horizontal
• A pesar de tener formación en ciencias de la computación, algunos lectores sienten confusión con |- y |=, así como con el significado en el nivel meta-sintáctico de las variables utilizadas
• Aunque agradecen la explicación, algunos lectores se preguntan por qué fue escrita en Stack Exchange y no en otra plataforma como lexi-lambda.github.io
• Se recomienda "Types and Programming Languages" de Benjamin C. Pierce como un buen libro de texto que cubre estos temas
• Algunos lectores llevaban años con curiosidad sobre este tema, pero no sabían cómo abordarlo
• Se menciona el Ada Reference Manual como un ejemplo de uso práctico de este tipo de sintaxis
• Elogios a una respuesta que empieza desde lo básico y va desarrollándose
• Se menciona como ejemplo que 𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍 sería algo sin sentido en la mayoría de los lenguajes, pero que en Python True + 2 sí es realmente un entero y equivale a 3