Como os tipos são provados — o sistema de tipos do TypeScript e a correspondência Curry–Howard

Resumo:

• Apresenta uma perspectiva que interpreta o sistema de tipos do TypeScript não como um simples verificador estático de tipos, mas como um sistema de provas da lógica.
• Com base na correspondência Curry–Howard (Type = Proposition, Program = Proof), explica conceitualmente por que a inferência de tipos é possível.
• Explica recursos do TypeScript, como tipos de função, generics, tipos condicionais e estreitamento de tipos, relacionando-os à implicação lógica, quantificação universal e análise de casos.
• Interpreta o processo de verificação de tipos não como aplicação de regras, mas como um processo de validação das relações entre proposições.
• Em vez de focar em detalhes de implementação, concentra-se no pano de fundo de design e na estrutura matemática do sistema de tipos do TypeScript.

Resumo detalhado:

1. Contexto: por que a inferência de tipos é possível?
   Em linguagens de tipagem estática, a inferência de tipos costuma ser explicada como um problema de implementação do tipo “como o compilador faz os tipos baterem”.
   Este texto dá um passo atrás e pergunta por que a inferência de tipos é, em sua origem, possível.
   Como resposta, apresenta a perspectiva de enxergar o sistema de tipos como um sistema de provas da lógica.

2. Base teórica: correspondência Curry–Howard
   Segundo a correspondência Curry–Howard, tipo (Type) corresponde a proposição (Proposition), e programa (Program) corresponde à prova (Proof) dessa proposição.
   Nessa perspectiva, a checagem de tipos é interpretada como o processo de verificar se um programa satisfaz uma determinada proposição.

3. Correspondência entre recursos do TypeScript e estruturas lógicas
   No texto, os principais recursos do TypeScript são relacionados da seguinte forma.

• tipo de função → implicação lógica (Implication)
• generics → quantificação universal (Universal Quantification)
• tipos condicionais / estreitamento de tipos → análise de casos (Case Analysis)
  Com isso, explica por que certas expressões de tipo soam naturais
  e por que alguns tipos são estruturalmente difíceis de representar.

4. Limites do sistema de tipos e escolhas de design
   Sob essa perspectiva, as restrições e limitações do TypeScript podem ser entendidas não como “falta de recursos”, mas como escolhas de design para manter a consistência lógica.
   O texto se concentra menos em técnicas ou truques práticos e mais em explicar sobre que filosofia e base matemática o sistema de tipos foi construído.

[pjh2568]

Foi muito divertido de ler, obrigado.

[devjeonghwan]

Embora digam que não é linting... para provar que a verificação de tipos é o cumprimento rigoroso de um contrato, esse contrato não deveria ser imposto no binário e em runtime? Caso contrário, acho que isso ainda não seria apenas um linting de tipos em um estado sintático flutuante?

[tsboard]

Foi um conteúdo impressionante. Foi a primeira vez que percebi que dá para enxergar isso por essa perspectiva. Também compartilhei o link do blog na empresa para recomendar aos meus colegas que dessem uma olhada. Obrigado!