Inferencia de tipo para declaraciones imperativas distintas de la asignación

En mi búsqueda de trabajos de investigación sobre sistemas de tipos para lenguajes imperativos, solo encuentro soluciones para un lenguaje con referencias mutables pero sin estructuras de control imperativo genuinas como operadores compuestos, bucles o condicionales.

Por lo tanto, no está claro cómo se puede implementar un lenguaje imperativo con inferencia de tipo parcial como http://rust-lang.org .

Los documentos no mencionan tipos parametrizados, como List of aporque los tipos parametrizados son una extensión trivial del sistema de tipos Hindley-Milner: solo el algoritmo de unificación debe extenderse, y el resto de la inferencia funciona como es. Sin embargo, las asignaciones no se pueden agregar trivialmente porque surgen paradojas, por lo que se deben aplicar técnicas especiales como la restricción del valor ML.

¿Puede recomendar algún documento o libro que describa un sistema de tipos para un lenguaje con bucles imperativos, condicionales, IO y declaraciones compuestas?

Si está buscando una referencia ordenada y funcional para la inferencia de tipos, estoy un poco parcial con respecto a la " Inferencia de tipos en contexto " de Gundry, McBride y McKinna de 2010 , aunque puede que esta no sea una buena guía para ninguna implementación real existente .

Creo que parte de la respuesta es que, más allá de la restricción de valor, realmente no hay tanta dificultad para adaptar la inferencia de tipo Hindley-Milner a los idiomas imperativos: si define e1; e2como azúcar sintáctico (fn _ => e2) e1y define while e1 do e2como azúcar sintáctico para whiledo e1 (fn () => e2), ¿dónde whiledoes un regular función recursiva

fun whiledo g f = if g then (f (); whiledo g f) else ();

entonces todo funcionará bien, incluida la inferencia de tipos.

En cuanto a que la restricción de valor es una técnica especial, me gusta la siguiente historia; Estoy bastante seguro de que lo recogí de Karl Crary. Considere el siguiente código, que la restricción de valor le impedirá escribir en ML:

let
   val x: 'a option ref = ref NONE
in
   (x := SOME 5; x := SOME "Hello")  
end

Compárelo con el siguiente código, que no tiene ningún problema:

let
   val x: unit -> 'a option ref = fn () => ref NONE
in
   (x () := SOME 5; x () := SOME "Hello")  
end

Sabemos lo que hace el segundo ejemplo: crea dos nuevas celdas de referencia que contienen NONE, luego coloca SOME 5la primera (a int option ref), luego coloca SOME "Hello"la segunda (a string option ref).

xx$\forall \alpha. \mbox{ref}(\mbox{option}(\alpha))$x$\Lambda \alpha. \mbox{ref}[\alpha](\mbox{NONE})$

Esto sugeriría que un comportamiento "bueno" del primer ejemplo es comportarse exactamente de la misma manera que el segundo ejemplo: instanciar la lambda de nivel de tipo dos veces diferentes. La primera vez que instanciamos xcon int, lo que hará que se x [int]evalúe a una celda de referencia NONEy luego SOME 5. La segunda vez que instanciamos xcon string, lo que hará que se x [string]evalúe en una celda de referencia ( ¡diferente! ) NONEY luego SOME "Hello". Este comportamiento es "correcto" (tipo seguro), pero definitivamente no es lo que un programador esperaría, y es por eso que tenemos la restricción de valor en ML, para evitar que los programadores se enfrenten a este tipo inesperado de comportamiento.

La tesis doctoral de Xavier Leroy es un buen comienzo.

Lo siento por responder mi propia pregunta, pero la referencia en cuestión es

Una propuesta para el estándar ML , Milner, 1983

La Parte 6 "Formularios Derivados Estándar" cubre el descortezado de las construcciones imperativas de manera bastante extensa. Y hasta ahora es la referencia más temprana de estas transformaciones en gran medida obvias que pude encontrar.