Inferir tipos de refinamiento

En el trabajo, se me ha encomendado la tarea de inferir cierta información sobre un lenguaje dinámico. Reescribo secuencias de declaraciones en letexpresiones anidadas , así:

return x; Z            =>  x
var x; Z               =>  let x = undefined in Z
x = y; Z               =>  let x = y in Z
if x then T else F; Z  =>  if x then { T; Z } else { F; Z }

Como comienzo a partir de información de tipo general y trato de deducir tipos más específicos, la elección natural son los tipos de refinamiento. Por ejemplo, el operador condicional devuelve una unión de los tipos de sus ramas verdadera y falsa. En casos simples, funciona muy bien.

Sin embargo, me encontré con un inconveniente al intentar inferir el tipo de lo siguiente:

function g(f) {
  var x;
  x = f(3);
  return f(x);
}

Que se reescribe a:

\f.
  let x = undefined in
    let x = f 3 in
      f x

HM y, en consecuencia, . El tipo real que quiero poder inferir es:$\mathtt{f} : \mathtt{Int} \to \mathtt{Int}$$\mathtt{g} : (\mathtt{Int} \to \mathtt{Int}) \to \mathtt{Int}$

$$\mathtt{g} : \forall \tau_1 \tau_2. \:(\mathtt{Int} \to \tau_1 \land \tau_1 \to \tau_2) \to \tau_2$$

Ya estoy usando dependencias funcionales para resolver el tipo de +operador sobrecargado , así que pensé que era una opción natural usarlos para resolver el tipo de fdentro g. Es decir, los tipos de fen todas sus aplicaciones juntas determinan de forma única el tipo de g. Sin embargo, como resultado, los fundeps no se prestan terriblemente bien a un número variable de tipos de fuentes.

De todos modos, la interacción del polimorfismo y la tipificación de refinamiento es problemática. Entonces, ¿hay un mejor enfoque que me estoy perdiendo? Actualmente estoy digiriendo "Tipos de refinamiento para ML" y agradecería más literatura u otros consejos.

Te has topado con el hecho de que la inferencia de invariantes estáticos para lenguajes de orden superior es bastante difícil en la práctica, además de ser indecidible en teoría. No estoy seguro de cuál es la respuesta definitiva a su pregunta, pero tenga en cuenta varias cosas:

• Los tipos de polimorfismo y refinamiento se comportan mal juntos, como ha notado, en particular se pierde la noción del tipo más general. Una consecuencia de esto es que los análisis basados ​​en tipos de refinamiento en presencia de polimorfismo pueden necesitar elegir entre el análisis de todo el programa (en oposición al análisis de composición) y el uso de heurísticas para decidir qué tipo desea asignar a su programa.

• Existe una fuerte relación entre inferir tipos de refinamiento y:

  1. Calcular la interpretación abstracta de su programa

  2. Calcular invariantes de bucle en un lenguaje imperativo.

Con esto en mente, aquí hay algunas referencias desorganizadas sobre la inferencia de tipos de refinamiento. Tenga en cuenta que hay muchos tipos diferentes de tipos de refinamiento: tiendo a estar más interesado en los refinamientos de los tipos de datos inductivos, por lo que esta lista puede estar sesgada en esa dirección.

1. Comience con los clásicos: Interpretación abstracta relacional de programas funcionales de orden superior por Cousot & Cousot. Esto explica cómo extender la interpretación abstracta a programas de orden superior usando semántica relacional.

2. Tipos de líquidos de Rhondon, Kawaguchi y Jhala. Este es un trabajo muy evolucionado, que combina HM y un tipo de refinamiento de predicados para inferir anotaciones de seguridad (por ejemplo, comprobaciones vinculadas a matrices) para programas de estilo ML. La inferencia procede en 2 pasos; el primero es la inferencia HM de anotaciones de tipo, que guían la elección de los refinamientos a realizar.

3. Probablemente también debería mencionar el trabajo de Fournet, Swarmy, Chen, Strub ... en , una extensión de que parece similar al enfoque de tipos líquidos, pero con el objetivo de verificar protocolos y algoritmos criptográficos para Computación distribuída. No estoy seguro de cuánto trabajo publicado hay sobre la inferencia de anotaciones en este caso.$F^*$$F^\#$

4. Hay un buen artículo de Chin y Khoo sobre la inferencia de un tipo específico de tipos de refinamiento: tipos con anotaciones de tamaño.

5. El lenguaje de programación ATS es un sistema que permite varios refinamientos y proporciona facilidades para escribir programas con ellos. Sin embargo, las anotaciones pueden ser arbitrariamente complejas (y, por lo tanto, indecidibles) y, por lo tanto, pueden requerir la interacción del usuario. Creo que hay una forma de inferencia para estos tipos, sin embargo, no estoy seguro de qué artículo recomendar.

6. Por último, pero no menos importante , el algoritmo del producto cartesiano , de Ole Agesen. Si bien no menciona explícitamente los tipos de refinamiento, este parece ser el trabajo más cercano a resolver el problema que parece tener. No se deje engañar por la mención del polimorfismo paramétrico en abstracto: buscan inferir tipos concretos , que son solo tuplas de posibles tipos atómicos. Se enfatiza la eficiencia. Recomiendo leer este artículo primero para ver si resuelve su problema.

Nota al margen: la inferencia de tipos en presencia de tipos de intersección puede ser muy indecidible: en la forma más simple, los términos con tipo de intersección son exactamente los términos fuertemente normalizantes. Camina suavemente alrededor de ellos :)$\lambda$