Sistema de tipo puro 📖 Wikipedia

Nos ramos da lógica matemática conhecidos como teoria da prova e teoria dos tipos, um sistema de tipos puro (PTS), anteriormente conhecido como sistema de tipos generalizado (GTS), é uma forma de cálculo lambda tipado que permite um número arbitrário de sortes e dependências entre quaisquer delas. O arcabouço pode ser visto como uma generalização do cubo lambda de Barendregt, no sentido de que todos os cantos do cubo podem ser representados como instâncias de um PTS com apenas duas sortes.^[1][2] De fato, Barendregt (1991) formulou seu cubo neste cenário.^[3] Sistemas de tipos puros podem obscurecer a distinção entre tipos e termos e colapsar a hierarquia de tipos, como é o caso do cálculo das construções, mas isso não é geralmente o caso, por exemplo, o cálculo lambda simplesmente tipado permite apenas que termos dependam de termos.

Sistemas de tipos puros foram introduzidos independentemente por Stefano Berardi (1988) e Jan Terlouw (1989).^[1][2] Barendregt os discutiu extensivamente em seus artigos subsequentes.^[4] Em sua tese de doutorado,^[5] Berardi definiu um cubo de lógicas construtivas análogo ao cubo lambda (essas especificações são não-dependentes). Uma modificação deste cubo foi posteriormente chamada de L-cubo por Herman Geuvers, que em sua tese de doutorado estendeu a correspondência de Curry–Howard a este cenário.^[6] Baseando-se nessas ideias, G. Barthe e outros definiram sistemas de tipos puros clássicos (CPTS) adicionando um operador de dupla negação.^[7] Similarmente, em 1998, Tijn Borghuis introduziu os sistemas de tipos puros modais (MPTS).^[8] Roorda discutiu a aplicação de sistemas de tipos puros à programação funcional; e Roorda e Jeuring propuseram uma linguagem de programação baseada em sistemas de tipos puros.^[9]

Os sistemas do cubo lambda são todos conhecidos por serem fortemente normalizantes. Sistemas de tipos puros em geral não precisam ser, por exemplo, o Sistema U do paradoxo de Girard não é. (Grosso modo, Girard encontrou sistemas puros nos quais se pode expressar a sentença "os tipos formam um tipo"). Além disso, todos os exemplos conhecidos de sistemas de tipos puros que não são fortemente normalizantes também não são (fracamente) normalizantes: eles contêm expressões que não têm formas normais, assim como o cálculo lambda não tipado

. É um grande problema em aberto na área se este é sempre o caso, isto é, se um PTS (fracamente) normalizante sempre tem a propriedade de normalização forte. Isso é conhecido como a conjectura de Barendregt–Geuvers–Klop (em homenagem a Henk Barendregt, Herman Geuvers e Jan Willem Klop).^[10]

Um sistema de tipos puro é definido por um triplo ${\textstyle ({\mathcal {S}},{\mathcal {A}},{\mathcal {R}})}$ onde ${\textstyle {\mathcal {S}}}$ é o conjunto de sortes, ${\textstyle {\mathcal {A}}\subseteq {\mathcal {S}}^{2}}$ é o conjunto de axiomas, e ${\textstyle {\mathcal {R}}\subseteq {\mathcal {S}}^{3}}$ é o conjunto de regras. A tipagem em sistemas de tipos puros é determinada pelas seguintes regras, onde ${\textstyle s}$ é qualquer sorte:^[4]

${\displaystyle {\frac {(s_{1},s_{2})\in {\mathcal {A}}}{\vdash s_{1}:s_{2}}}\quad {\text{(axioma)}}}$

${\displaystyle {\frac {\Gamma \vdash A:s\quad x\notin {\text{dom}}(\Gamma )}{\Gamma ,x:A\vdash x:A}}\quad {\text{(início)}}}$

${\displaystyle {\frac {\Gamma \vdash A:B\quad \Gamma \vdash C:s\quad x\notin {\text{dom}}(\Gamma )}{\Gamma ,x:C\vdash A:B}}\quad {\text{(enfraquecimento)}}}$

${\displaystyle {\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash B:s_{2}\quad (s_{1},s_{2},s_{3})\in {\mathcal {R}}}{\Gamma \vdash \Pi x:A.B:s_{3}}}\quad {\text{(produto)}}}$

${\displaystyle {\frac {\Gamma \vdash C:\Pi x:A.B\quad \Gamma \vdash a:A}{\Gamma \vdash Ca:B[x:=a]}}\quad {\text{(aplicação)}}}$

${\displaystyle {\frac {\Gamma ,x:A\vdash b:B\quad \Gamma \vdash \Pi x:A.B:s}{\Gamma \vdash \lambda x:A.b:\Pi x:A.B}}\quad {\text{(abstração)}}}$

${\displaystyle {\frac {\Gamma \vdash A:B\quad B=_{\beta }B'\quad \Gamma \vdash B':s}{\Gamma \vdash A:B'}}\quad {\text{(conversão)}}}$

As seguintes linguagens de programação têm sistemas de tipos puros:

• SAGE^[11]
• Yarrow^[12]
• Henk 2000^[13]
• Haskell desde a versão 8 do GHC.^[14][15]

• Sistema U – um exemplo de PTS inconsistente
• Cálculo λμ usa uma abordagem diferente para controle do que CPTS

• Schmidt, David A. (1994). «§ 8.3 Generalized Type Systems». The structure of typed programming languages. [S.l.]: MIT Press. pp. 255–8. ISBN 0-262-19349-3 

• Sistema de tipos puro in nLab
• Jones, Roger Bishop (1999). «Visão geral de Sistemas de Tipos Puros»