Algoritmos de verificação de tipo

19

Estou iniciando uma pesquisa bibliográfica pessoal sobre algoritmos de verificação de tipo e quero algumas dicas. Quais são os algoritmos, estratégias e técnicas gerais de verificação de tipo mais usados?

Estou particularmente interessado em algoritmos complexos de verificação de tipo que foram implementados em linguagens tipicamente fortemente estáticas amplamente conhecidas, como, por exemplo, C ++, Java 5+, Scala ou outros. IE, algoritmos de verificação de tipo que não são muito simples devido à digitação muito simples da linguagem subjacente (como Java 1.4 e abaixo).

Não estou interessado em um idioma específico X, Y ou Z. Estou interessado em algoritmos de verificação de tipo, independentemente do idioma que eles segmentam. Se você fornecer uma resposta como "a linguagem L da qual você nunca ouviu falar e que é fortemente digitada e a digitação é complexa, possui um algoritmo de verificação de tipo que executa A, B e C marcando X e Y usando o algoritmo Z" ou "the As estratégias X e Y usadas para Scala e uma variante Z de A usada para C # são legais por causa dos recursos R, S e T que funcionam dessa maneira ", então as respostas são boas.

Victor Stafusa
fonte
3
Talvez você deva editar esta pergunta para perguntar sobre a verificação de tipo para um idioma específico. Perguntas abertas e em estilo de lista geralmente são desencorajadas no SE (embora esse site em particular ainda não tenha uma política). Além disso: <type-system-elitist> O sistema de tipos Java não é complexo </type-system-elitist>.
sepp2k
3
Talvez a questão possa ser reformulada para ser mais específica, mas não acho que deva ser encerrada.
9608 Dave Clarke
1
@ sepp2k: Eu sei que é um pouco amplo, mas terminou dessa maneira porque não quero limitar a utilidade das respostas. BTW, eu não entendi o que você quer dizer com "<type-system-elitist> O sistema de tipos Java não é complexo </type-system-elitist>". O sistema 1.4 e abaixo do Java era simples, mas com genéricos no Java 5, ficou muito mais complexo.
Victor Stafusa
2
Pedir um idioma específico tornaria a pergunta mais inadequada para este site, imho. A pergunta talvez deva pedir técnicas gerais.
Raphael
1
@ Victor Uma ferramenta básica são Gramáticas de Atributos . Talvez você não consiga fazer todas as coisas más que puder imaginar com elas, mas elas são um bom ponto de partida.
Raphael

Respostas:

13

A maioria das pesquisas não publica realmente os algoritmos de verificação de tipo para linguagens de programação completas. Você encontrará algumas formalizações de grande parte dos sistemas de tipos para linguagens de programação completas, como o trabalho de Drossopoulou e Eisenbach para Java ou o trabalho de Nipkov et al em C ++ . Mais frequentemente, porém, você encontrará apenas os sistemas de tipos para alguma parte principal da linguagem (Featherweight Java é um exemplo) ou para os conceitos principais de uma linguagem, como a abordagem de inferência de tipo local do scala .

Em conferências como POPL e ICFP, você encontrará muitos algoritmos de verificação de tipos para tipos específicos de sistemas de tipos e novas abordagens, como a verificação de tipos bidirecional e tridirecional .

Em geral, você provavelmente precisará conhecer o algoritmo Damas-Milner , a inferência de tipo local, a verificação de tipo bidirecional e tridirecional e expandir a partir daí, seguindo as referências nos artigos e usando o google scholar para descobrir quais documentos os citam e desenvolver as abordagens descritas. Além disso, como sugerido acima, conferências como POPL, ICPF, ESOP e até ECOOP e OOPSLA terão documentos relevantes para sua busca.

Dave Clarke
fonte
Afaik, o sistema de tipos da Scala foi desenvolvido em projetos de pesquisa e, portanto, é publicado. O compilador também é de código aberto. Também não investiguei.
Raphael
Não há necessidade de inferir; Eu sei que existem artigos publicados sobre o sistema de tipos de Scala. Essa reivindicação é facilmente verificada pela pesquisa . Além disso, conto o código-fonte do compilador como publicação suficiente no algoritmo (desde que esteja incluído nas fontes; presumo que sim, mas não verifiquei). Minha afirmação inicial foi ambígua, é verdade, mas sua reação parece injustificada.
Raphael
2

Uma ferramenta básica são gramáticas de atributos . Talvez você não consiga fazer todas as coisas más que puder imaginar com elas, mas elas são um bom ponto de partida.

Essencialmente, você pode percorrer a árvore de sintaxe abstrata de um programa de cima para baixo e / ou de baixo para cima e passar informações. Assim, por exemplo, você pode passar informações do tipo de escopo global (por exemplo, classes e seus membros) para baixo e determinar o tipo de expressões recursivamente, ou seja, de baixo para cima, passando os tipos resultantes para cima.

Encontre algumas explicações e exemplos nos slides aqui (capítulo 5).

Rafael
fonte
Alguém tem uma referência melhor? Acho que preciso comprar o Dragonbook ou Wilhelm / Maurer um dia desses ...
Raphael
1
A ferramenta JastAdd é um excelente e moderno sistema de compilador de compiladores, baseado em gramáticas de atributos de referência. Nós o usamos em vários projetos.
68660 Dave