Quais são os limites da inferência de tipos?

Question

Quais são os limites da inferência de tipos? Quais sistemas do tipo não têm algoritmo geral de inferência?

Answer 1

Joe Wells mostrou que a inferência de tipos é indecidível para sistema F, que é o cálculo lambda mais básico polimórfica, descobriu independentemente por Girard e Reynolds. Este é o resultado mais importante mostrando os limites da inferência de tipos.

Aqui está um problema importante que é ainda em aberto: qual é a melhor maneira de integrar Tipos Generalized algébrica de dados em Hindley-Milner inferência de tipos? Todos os anos, Simon Peyton Jones surge com uma nova resposta, que é supostamente melhor do que a resposta do ano anterior. Eu não li a versão de Março de 2009 e por isso não posso dizer se eu acredito que será definitiva.

Answer 2

Um sistema de tipo dependente valor (ou em suma, sistema de tipo dependente) pode descrever tipos que dizem coisas como: "No tempo de avaliação (runtime), o valor desta variável será sempre igual ao valor dessa variável , que é calculado com um processo de avaliação diferente". deduzir automaticamente este tipo de código implica provas automáticas de teoremas. Se o conjunto de teoremas você pode expressar é restrito àqueles automaticamente provável, isso não seria um problema, mas no caso das línguas dependente tipado, isso geralmente não é o caso.

sistemas Então dependente digitadas não pode ter geral (e completo) inferência de tipos.

Estou certo de que alguém pode fornecer uma resposta formal e moral completa ...