Como ler a notação de sistemas de tipos?

• Este artigo traz uma explicação detalhada sobre como ler e entender a notação de sistemas de tipos em linguagens de programação.
• A notação de sistemas de tipos é uma expressão matemática usada em artigos e papers sobre sistemas de tipos.
• A notação usada para descrever sistemas de tipos varia conforme a apresentação, mas a maioria compartilha muitos elementos em comum.
• O sistema de tipos aplicado a uma linguagem de programação é um sistema sintático, ou seja, um conjunto de regras que atua sobre a sintaxe da linguagem.
• Essa notação tem origem na lógica formal e é usada para construir provas formais sobre as propriedades de um sistema.
• O artigo também discute os conceitos de relação, julgamento, axioma e regra de inferência na notação de sistemas de tipos.
• A relação de tipagem normalmente é escrita como e:τ e pode ser lida como "e tem o tipo τ".
• O julgamento de tipagem é escrito com a notação ⊢e:τ⊢, em que ⊢ pode ser lido como "a afirmação a seguir é verdadeira".
• O artigo também explica em detalhes os conceitos de variáveis, contexto e ambiente na notação de sistemas de tipos.
• O contexto, ou ambiente de tipos, é representado por Γ na notação.
• O artigo também aborda outros padrões de notação e considerações comuns, como layout de regras de inferência, condições laterais, subtipagem, múltiplos contextos e verificação bidirecional de tipos.
• Este artigo é um guia abrangente para entender a notação de sistemas de tipos, especialmente para quem está começando nesse conceito.

[GN⁺]

Comentários do Hacker News

• Discussão sobre a notação de sistemas de tipos em artigos de ciência da computação, com uma explicação básica sobre notação BNF, regras de inferência etc.
• A origem da notação pode ser rastreada até Frege, e os elementos centrais são o símbolo de catraca e a linha horizontal
• Apesar de serem formados em ciência da computação, alguns leitores acham confuso o significado de |- e |=, bem como o sentido, em nível metassintático, das variáveis usadas
• A explicação é apreciada, mas alguns leitores se perguntam por que foi escrita no Stack Exchange e não em outra plataforma, como lexi-lambda.github.io
• "Types and Programming Languages", de Benjamin C. Pierce, é recomendado como um bom livro-texto que aborda esse conteúdo
• Alguns leitores tinham curiosidade sobre esse tema há anos, mas não sabiam como começar a estudá-lo
• O Ada Reference Manual é mencionado como um exemplo prático de uso desse tipo de sintaxe
• Elogios à resposta por começar pelo básico e ir desenvolvendo o assunto
• 𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍 é algo sem sentido na maioria das linguagens, mas, em Python, True + 2 realmente é um inteiro e é igual a 3