Sistemas de Tipos para Linguagens Declarativas
Mário Florido
Departamento de Ciência de Computadores & LIACC
Faculdade de Ciências, Universidade do Porto
Rua do Campo Alegre, 823 4150 Porto, Portugal
Janeiro de 1998
Resumo
Esta tese tem como objectivo desenvolver caracterizações semânticas
precisas de sistemas de tipos descritivos para linguagens
declarativas.
A nossa tese é a de que as relações sintácticas entre tipos e termos
resultam de relações semânticas muito mais fortes do que a
integridade, usualmente exigida aos sistemas de tipos. Temos como
interesse principal definir os sistemas de tipos a partir de relações
semânticas entre tipos e termos e não definir os sistemas e,
posteriormente, arranjar uma semântica que garanta boas propriedades.
O critério semântico usado normalmente para relacionar termos e tipos
é a integridade. Essa relação semântica é apresentada para os
seguintes sistemas de tipos:
- O sistema de tipos simples para o lambda-calculus;
- O sistema de tipos da linguagem ML;
- Os sistemas de tipos com intersecções;
- Várias metodologias para a definição de sistemas de tipos no
paradigma da programação em lógica.
Baseados na relação semântica entre termos e tipos definimos, para
cada termo, um conjunto de restrições nos tipos que garantem a sua
validade semântica.
Atendendo à visão de Curry de tipos como
descrições, definimos condições semânticas necessárias ao carácter
descritivo dos tipos. Demonstramos que os sistemas de Curry e da
linguagem ML são integros com respeito a essa caracterização
semântica. O mesmo não acontece nos sistemas de tipos com
intersecções, e usando essa propriedade explicamos, sob o ponto de
vista semântico, algumas anomalias destes sistemas.
Baseados em propriedades semânticas dos sistemas de tipos
identificadas no lambda-calculus, definimos um critério semântico
de classificação de tipos para programas em lógica. Usamos esse
critério para demonstrar a adequação de uma linguagem: a linguagem
regular determinística, e a não adequação de outra: a linguagem
regular, para denotar tipos de programas em lógica.
