Quais são os sistemas de tipos conhecidos mais fortes para os quais a inferência é decidível?

É sabido que a inferência do tipo Hindley-Milner (o -calculus de digitação simples com polimorfismo) tem uma inferência de tipo decidível: você pode reconstruir os tipos de princípio para qualquer programa sem nenhuma anotação.$\lambda$

A adição de classes de tipo no estilo Haskell parece preservar essa decisão, mas adições adicionais tornam a inferência sem anotações indecidíveis (famílias de tipos, GADTs, tipos dependentes, tipos Rank-N, System etc.)$\omega$

Estou me perguntando: quais são os sistemas de tipos conhecidos mais fortes, com inferência completamente decidível? Vai ficar em algum lugar entre Hindley-Milner (completamente decidível) e dependente (completamente indecidível). Existem aspectos das TDs que podem ser adicionados que preservam a decidibilidade da inferência? Que pesquisa foi feita para ver até onde isso pode ser levado?

Percebo que não existe um único sistema mais forte, que provavelmente existem pequenas e infinitas mudanças incrementais que podem ser adicionadas ao HM mantendo a inferência. Mas há provavelmente alguns candidatos práticos de sistemas que foram descobertos.

Edit: dado que não existe um sistema "mais forte", aceitarei uma resposta que descreve os notáveis sistemas que estendem Hindley Milner com inferência decidida. Os exemplos podem ser Tipos de líquidos, Grau 2, etc.

[EDIT: Voilà algumas palavras em cada]

Existem várias maneiras de estender a inferência do tipo HM. Minha resposta é baseada em muitas tentativas, mais ou menos bem-sucedidas, de implementar algumas delas. O primeiro que encontrei foi o polimorfismo paramétrico . Os sistemas de tipos que tentam estender o HM nessa direção tendem para o Sistema F e, portanto, requerem anotações de tipo. Duas extensões notáveis ​​nessa direção que me deparei são:

• HMF, permite a inferência de tipo para todos os tipos System-F, o que significa que você pode ter uma quantificação universal "no meio" de um tipo, sua aparência não está implicitamente situada no escopo mais alto, como nos tipos polimórficos HM. O documento afirma claramente que não existe uma regra clara sobre quantas e onde anotações de tipo podem ser necessárias. Além disso, sendo os tipos do Sistema F, os termos geralmente não têm um tipo principal.

• O MLF não é apenas uma extensão do HM, é também uma extensão do Sistema F que recupera a propriedade de tipo principal do HM, introduzindo um tipo de quantificação limitada sobre os tipos. Uma comparação foi feita pelos autores, o MLF é estritamente mais poderoso que o HMF e as anotações são necessárias apenas para parâmetros usados ​​polimorficamente.

Outra maneira de estender o HM é através da variação do domínio de restrição.

• HM (X) é Hindley-Milner parametrizado em um domínio de restrição X. Nessa abordagem, o algoritmo HM gera as restrições enviadas a um solucionador de domínio para X. Para o HM usual, o solucionador de domínio é o procedimento de unificação e o domínio consiste em do conjunto de termos construídos a partir dos tipos e das variáveis ​​de tipo.
  Outro exemplo para X pode ser as restrições expressas no idioma da aritmética de Presburger (nesse caso, a inferência / verificação de tipo é decidível) ou no idioma da aritmética de Peano (não é mais decidível). X varia ao longo de um espectro de teorias, cada uma com seus próprios requisitos em relação à quantidade e localização das anotações de tipo necessárias e variando de nenhuma a todas elas.

• As classes de tipo de Haskell também são um tipo de extensão do domínio de restrição, adicionando predicados de tipo do formulário MyClass(MyType)(o que significa que existe uma instância de MyClass para o tipo MyType).
  As classes de tipo preservam a inferência de tipo porque são basicamente conceitos (quase) ortogonais que implementam polimorfismo adhoc .
  Como exemplo, tome um símbolo valdo tipo val :: MyClass a => apara o qual você pode ter instâncias MyClass A, MyClass Betc. Quando você se referir a esse símbolo em seu código, é realmente porque a inferência de tipos já é realizado que o compilador pode inferir qual instância da classe para uso. Isso significa que o tipo de valdepende do contexto em que é usado. É também por isso que executar uma única valinstrução leva a umambiguous type error : o compilador não pode inferir nenhum tipo com base no contexto.

Para sistemas de tipos mais avançados, como GADTs, famílias de tipos, tipos dependentes, System (F) ω, etc., o tipo não é mais "tipos", eles se tornam objetos computacionais complexos. Por exemplo, significa que dois tipos que não parecem iguais não são necessariamente diferentes. Portanto, a igualdade de tipos não se torna trivial.

Para dar um exemplo da complexidade real, vamos considerar o tipo dependente de lista: NList a nonde aestá o tipo de objetos na lista e nseu comprimento.
A função de acréscimo teria o tipo append :: NList a n -> NList a m -> NList a (n + m)e a função zip seria zip :: NList a n -> NList b n -> NList (a, b) n.
Imagine agora que temos a lambda \a: NList t n, b: NList t m -> zip (append a b) (append b a). Aqui, o primeiro argumento do zip é do tipo NList t (n + m)e o segundo do tipo NList t (m + n).
Quase o mesmo, mas, a menos que o verificador de tipos saiba que "+" é comutado em números naturais, ele deve rejeitar a função porque (n + m) não é literalmente (m + n). Não se trata mais de inferência / verificação de tipo, mas de prova de teoremas.

Os tipos líquidos parecem estar fazendo alguma inferência de tipo dependente. Mas, pelo que entendi, não é realmente um tipo dependente, mais algo como os tipos comuns de HM, nos quais é feita uma inferência adicional para calcular limites estáticos.

Eu espero que isso ajude.