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.Fundeps y GADT: ¿Cuándo es decidible la verificación de tipo?
Preferiría citas si las tiene para que pueda leer/entender las explicaciones.
Gracias!
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 :-)
Ese es un buen punto. Así que supongo que estoy interesado en cuándo es decidible la inferencia de tipo GHC de las GADT. –
Probablemente ya haya visto esto, pero hay una colección de documentos sobre este tema en la investigación de Microsoft: Type Checking papers. El primero describe el algoritmo decidible realmente utilizado en el compilador Haskell de Glasgow.
Los documentos a los que se hace referencia son buenos documentos, pero no parecen responder a mi pregunta. –
Esta pregunta podría dirigirse mejor a los autores del trabajo de investigación. Es un poco esotérico para Stack Overflow. (Siempre he tenido un gran éxito contactando a los investigadores para comentar. Usualmente están extasiados * cualquiera * está leyendo su trabajo.) –
Creo que esta actitud (que las preguntas teóricas no tienen que ver con un foro pragmático) es dañina y obsoleta. Los enfoques pragmáticos deberían estar abiertos a las nuevas tecnologías, porque esas tecnologías pueden mejorar las actividades diarias en el futuro cercano. por ejemplo: características funcionales en C#/python. – rcreswick
Dicho esto, el comentario de Chirs probablemente sea correcto, prácticamente hablando. Desearía que no fuera así. – rcreswick