Abstract
A teoria de tipos é o ramo da matemática e da lógica com o intuito de classificar as entidades de um conjunto chamado tipo.
A principal aplicabilidade da Teoria de Tipos é na computação, em específico no desenvolvimento de sistema de tipos em linguagens de programação.
A definição de “sistema de tipos” não é exata, porém a mais consolidada na comunidade é dada por Benjamin C. Pierce - na obra Types and Programming Languages, MIT Press, 2002 - com a seguinte definição sobre Teoria de Tipos:
Quote
Um sistema de tipos é um método sintático tratável para provar a isenção de certos comportamentos em um programa através da classificação de frases de acordo com as espécies de valores que elas computam.
Em outras palavras, um sistema de tipos categoriza os valores de um programa em conjuntos denominados tipos (isso é o que chamamos de “atribuição de tipos”) e proíbe certos comportamentos no programa com base nos tipos atribuídos durante esse processo.
Referências
Teoria dos tipos - https://pt.wikipedia.org/wiki/Teoria_dos_tipos