Inferência de Tipos e Resolução de Restrições
Sandra Maria Mendes Alves
Mestrado em Informática - Ramo de Sistemas e Redes
Departamento de Ciência de Computadores
Faculdade de Ciências da
Universidade do Porto
Setembro 2001
Resumo
Nesta dissertação apresentamos uma implementação
do esquema geral de algoritmos de inferência de tipos HM(X), usando
Prolog e CHR (Constraint Handling Rules). O processo de inferência
de tipos pode envolver mecanismos de resolução de restrições.
Embora as restrições de igualdade possam ser resolvidas por
um algoritmo de unificação, outros tipos de restrições
podem necessitar de algoritmos mais complexos. Na nossa implementação,
as restrições de igualdade entre tipos são resolvidas
por unificação, usando a unificação do Prolog
com
occur-check, e outros tipos de restrições são
resolvidas por resolutores específicos implementados em CHR. Com
base no esquema geral de algoritmos de inferência de tipos HM(X), implementamos:
- Um algoritmo geral de inferência de tipos;
- Instâncias para:
- o sistema de Damas-Milner;
- o sistema com estruturas com campos de Ohori;
- o sistema de Nipkow e Prehofer com classes de tipos;
- o sistema O de Odersky, Wadler e Wehr.
Na nossa implementação, a diferença entre os aspectos
gerais dos algoritmos de inferência de tipos e os módulos de
resolução de restrições torna-se mais clara quando
comparada com outras implementações dos mesmos sistemas de
tipos, normalmente feitas numa linguagem de programação funcional.
As regras CHR revelaram-se um modo natural de especificar os mecanismos de
simplificação.
