haskell - Fundeps y GADT: ¿Cuándo es decidible la verificación de tipo?

type-inference type-systems

Question

Estaba leyendo un trabajo de investigación sobre Haskell y cómo se implementa HList y me pregunto cuándo las técnicas descritas son y no son decidibles para el verificador de tipos. Además, como puedes hacer cosas similares con las GADT, me preguntaba si la verificación de tipo GADT siempre es decidible.

Preferiría citas si las tienes para que pueda leer / entender las explicaciones.

¡Gracias!

Answer 1

Probablemente ya haya visto esto, pero hay una colección de documentos sobre este tema en la investigación de Microsoft: Documentos de verificación de tipo . El primero describe el algoritmo decidible realmente utilizado en el compilador Haskell de Glasgow.

Answer 2

Creo que la verificación de tipo GADT siempre es decidible; su inferencia es indecidible, ya que requiere una unificación de orden superior. Pero un verificador de tipo GADT es una forma restringida de los verificadores de prueba que se ven en, por ejemplo. Coq, donde los constructores construyen el término de prueba. Por ejemplo, el ejemplo clásico de incrustación de cálculo lambda en GADT tiene un constructor para cada regla de reducción , por lo que si desea encontrar la forma normal de un término, debe indicarle qué constructores lo llevarán a él. El problema de detención se ha movido a las manos del usuario :-)