¿Cuáles son los sistemas de tipos conocidos más fuertes para los que la inferencia es decidible?

Es bien sabido que la inferencia de tipo Hindley-Milner (el cálculo tipo simple con polimorfismo) tiene una inferencia de tipo decidible: puede reconstruir tipos de principios para cualquier programa sin ninguna anotación.$\lambda$

Agregar clases de tipo de estilo Haskell parece preservar esta capacidad de decisión, pero las adiciones adicionales hacen que la inferencia sin anotaciones sea indecidible (familias de tipos, GADT, tipos dependientes, tipos de rango N, System , etc.)$\omega$

Me pregunto: ¿cuáles son los sistemas de tipos más fuertes conocidos con inferencia completamente decidible? Se ubicará en algún lugar entre Hindley-Milner (completamente decidible) y los tipos dependientes (completamente indecidible). ¿Hay aspectos de los DT que se pueden agregar que preserven la capacidad de decisión de inferencia? ¿Qué investigaciones se han hecho para ver hasta dónde puede llegar esto?

Me doy cuenta de que no hay un solo sistema más fuerte, que probablemente hay infinitos pequeños cambios incrementales que se pueden agregar a HM manteniendo la inferencia. Pero es probable que se descubran algunos candidatos prácticos de sistemas.

Editar: dado que no existe un sistema "más fuerte", aceptaré una respuesta que describa los sistemas notables que extienden a Hindley Milner con una inferencia decidible. Los ejemplos podrían ser Tipos líquidos, Rango 2, etc.

[EDITAR: Voilà algunas palabras en cada uno]

Hay varias formas de extender la inferencia de tipo HM. Mi respuesta se basa en muchos intentos, más o menos exitosos, de implementar algunos de ellos. El primero con el que me topé es el polimorfismo paramétrico . Los sistemas de tipos que intentan extender HM en esta dirección tienden hacia el Sistema F y, por lo tanto, requieren anotaciones de tipo. Dos extensiones notables en esta dirección que encontré son:

• HMF, permite la inferencia de tipos para todos los tipos de System-F, lo que significa que puede tener una cuantificación universal "en el medio" de un tipo, su apariencia no está implícitamente situada en el ámbito más alto como para los tipos polimórficos HM. El documento establece claramente que no existe una regla clara sobre cuántas y dónde pueden ser necesarias las anotaciones de tipo. Además, los tipos son los del Sistema F, los términos generalmente no tienen un tipo principal.

• MLF no es solo una extensión de HM, también es una extensión del Sistema F que recupera la propiedad de tipo principal de HM al introducir un tipo de cuantificación limitada sobre los tipos. Los autores han hecho una comparación, MLF es estrictamente más potente que HMF y las anotaciones solo son necesarias para los parámetros utilizados polimórficamente.

Otra forma de extender HM es a través de la variación del dominio de restricción.

• HM (X) es Hindley-Milner parametrizado sobre un dominio de restricción X. En este enfoque, el algoritmo HM genera las restricciones que se envían a un solucionador de dominio para X. Para el HM habitual, el solucionador de dominio es el procedimiento de unificación y el dominio consiste del conjunto de términos construidos a partir de los tipos y las variables de tipo.
  Otro ejemplo para X podría ser las restricciones expresadas en el lenguaje de la aritmética de Presburger (en cuyo caso, la inferencia / verificación de tipo es decidible) o en el lenguaje de la aritmética de Peano (ya no es decidible). X varía a lo largo de un espectro de teorías, cada una con sus propios requisitos con respecto a la cantidad y localización de anotaciones de tipo necesarias y que van desde nada en absoluto hasta todas ellas.

• Las clases de tipos de Haskell también son un tipo de extensión del dominio de restricción al agregar predicados de tipo de la forma MyClass(MyType)(lo que significa que existe una instancia de MyClass para el tipo MyType).
  Las clases de tipos preservan la inferencia de tipos porque son básicamente conceptos (casi) ortogonales que implementan polimorfismo adhoc .
  Como ejemplo, tome un símbolo valde tipo val :: MyClass a => apara el que pueda tener instancias MyClass A, MyClass Betc. Cuando hace referencia a ese símbolo en su código, en realidad es porque la inferencia de tipo ya se realizó que el compilador puede inferir qué instancia de la clase usar. Esto significa que el tipo de valdepende del contexto en el que se utiliza. Es por eso que ejecutar una sola valdeclaración lleva a unaambiguous type error : el compilador no puede inferir ningún tipo basado en el contexto.

Para sistemas de tipos más avanzados como GADT, familias de tipos, tipos dependientes, Sistema (F) ω, etc., los tipos ya no son "tipos" sino que se convierten en objetos computacionales complejos. Por ejemplo, significa que dos tipos que no se ven iguales no son necesariamente diferentes. Entonces la igualdad de tipos no se vuelve trivial (en absoluto).

Para darle un ejemplo de la complejidad real, consideremos el tipo de lista dependiente: NList a ndónde aestá el tipo de objetos en la lista y nsu longitud.
La función append tendría tipo append :: NList a n -> NList a m -> NList a (n + m)y la función zip sería zip :: NList a n -> NList b n -> NList (a, b) n.
Imagina ahora que tenemos la lambda \a: NList t n, b: NList t m -> zip (append a b) (append b a). Aquí el primer argumento de zip es de tipo NList t (n + m)y el segundo de tipo NList t (m + n).
Casi lo mismo, pero a menos que el verificador de tipos sepa que "+" conmuta en números naturales, debe rechazar la función porque (n + m) no es literalmente (m + n). Ya no se trata de inferencia de tipo / verificación de tipo, se trata de probar el teorema.

Los tipos líquidos parecen estar haciendo alguna inferencia de tipo dependiente. Pero, según tengo entendido, no es realmente un tipo dependiente, más bien algo parecido a los tipos HM habituales en los que se hace una inferencia adicional para calcular los límites estáticos.

Espero que esto ayude.