Fundeps e GADTs:Quando a verificação de tipo é decidível?

Question

Eu estava lendo um artigo de pesquisa sobre Haskell e como o HList é implementado e me perguntando quando as técnicas descritas são ou não decidíveis para o verificador de tipo.Além disso, como você pode fazer coisas semelhantes com GADTs, gostaria de saber se a verificação de tipo do GADT é sempre decidível.

Eu preferiria citações, se você as tiver, para que eu possa ler/entender as explicações.

Obrigado!

Answer 1

Acredito que a verificação do tipo GADT é sempre decidível;é a inferência que é indecidível, pois requer uma unificação de ordem superior.Mas um verificador do tipo GADT é uma forma restrita dos verificadores de prova que você vê, por exemplo.Coq, onde os construtores constroem o termo de prova.Por exemplo, o exemplo clássico de incorporação de cálculo lambda em GADTs tem um construtor para cada regra de redução, portanto, se você quiser encontrar a forma normal de um termo, precisará informar quais construtores o levarão até ele.O problema da parada foi transferido para as mãos do usuário :-)

Answer 2

Você provavelmente já viu isso, mas há uma coleção de artigos sobre esse assunto na pesquisa da Microsoft: Tipo Verificando papéis.O primeiro descreve o algoritmo decidível realmente usado no compilador Glasgow Haskell.