Restricción de valor

En los lenguajes de programación con inferencia de tipos Hindley-Milner y características imperativas , en particular la familia de lenguajes de programación ML , la restricción de valores implica que las declaraciones solo se generalizan polimórficamente si son valores sintácticos (también llamados no expansivos ). Esta restricción impide que las celdas de referencia contengan valores de diferentes tipos y preserva la seguridad de tipos .

En el sistema de tipos Hindley-Milner , las expresiones pueden tener múltiples tipos mediante polimorfismo paramétrico . Sin embargo, asignar ingenuamente múltiples tipos a las referencias rompe la seguridad de tipos . Las siguientes ^{[ 1 ]} son ​​reglas de tipado para referencias y operadores relacionados en lenguajes tipo ML .

${\displaystyle {\begin{aligned}{\mathtt {ref}}&:\forall \alpha .\alpha \to (\alpha \ {\mathtt {ref}})\\{\mathtt {!}}&:\forall \alpha .(\alpha \ {\mathtt {ref}})\to \alpha \\{\mathtt {:=}}&:\forall \alpha .(\alpha \ {\mathtt {ref}})\to \alpha \to {\mathtt {unidad}}\end{aligned}}}$

Los operadores tienen la siguiente semántica :${\textstyle {\mathtt {ref}}}$toma un valor y crea una referencia que contiene ese valor,${\textstyle {\mathtt {!}}}$(desreferencia) toma una referencia y lee el valor en esa referencia, y${\textstyle {\mathtt {:=}}}$(asignación) actualiza una referencia para que contenga un nuevo valor y devuelve un valor del tipo de unidad . Dado esto, el siguiente programa ^{[ 1 ]} aplica incorrectamente una función destinada a enteros a un valor booleano.

let val c = ref ( fn x => x ) in c := ( fn x => x + 1 ); !c true end

El programa anterior realiza comprobaciones de tipo utilizando Hindley-Milner porque cse le da el tipo.${\textstyle \forall \alpha .(\alpha \to \alpha )\ {\mathtt {ref}}}$, que luego se instancia para ser del tipo${\textstyle ({\mathtt {int}}\to {\mathtt {int}})\ {\mathtt {ref}}}$al escribir la tarea yc := (fn x => x + 1)${\textstyle ({\mathtt {bool}}\to {\mathtt {bool}})\ {\mathtt {ref}}}$ref al escribir la desreferencia !c true.

Bajo la restricción de valor, los tipos de expresiones de let bound solo se generalizan si las expresiones son valores sintácticos . En su artículo, ^{[ 1 ]} Wright considera que los siguientes son valores sintácticos: constantes, variables,${\textstyle \lambda }$-expresiones y constructores aplicados a valores. Las aplicaciones de funciones y operadores no se consideran valores. En particular, las aplicaciones de la${\displaystyle {\mathtt {ref}}}$Los operadores no se generalizan. Es seguro generalizar las variables de tipo de valores sintácticos porque su evaluación no puede causar efectos secundarios como escribir en una referencia.

El ejemplo anterior es rechazado por el verificador de tipos bajo la restricción de valor de la siguiente manera.

• Primero cse da el tipo${\textstyle (\alpha \to \alpha )\ {\mathtt {ref}}}$Este tipo no está generalizado y${\textstyle \alpha }$es una variable libre en el contexto de tipado para el cuerpo del enlace let.
• Cuando se escribe la asignación, el tipo cse modifica en el contexto de escritura para ser de tipo${\textstyle ({\mathtt {int}}\to {\mathtt {int}})\ {\mathtt {ref}}}$mediante la unificación .
• La desreferenciación !cse tipifica como${\displaystyle {\mathtt {int}}\to {\mathtt {int}}}$, pero se aplica a un valor de tipo${\textstyle {\mathtt {bool}}}$y el verificador de tipos rechaza el programa.

• Inferencia del tipo Hindley-Milner

• Mads Tofte (1988). Semántica operacional e inferencia de tipos polimórficos . Tesis doctoral.
• M. Tofte (1990). "Inferencia de tipos para referencias polimórficas".
• O'Toole (1990). "Reglas de abstracción de tipos para referencia: una comparación de cuatro que han alcanzado notoriedad".
• Xavier Leroy y Pierre Weis (1991). "Inferencia y asignación de tipos polimórficos". POPL '91.
• AK Wright (1992). "Tipado de referencias mediante inferencia de efectos".
• My Hoang, John C. Mitchell y Ramesh Viswanathan (1993). "Polimorfismo débil ML-NJ estándar y construcciones imperativas".
• Andrew Wright (1995). " Polimorfismo imperativo simple ". En LISP y computación simbólica , págs.  343-356.
• Jacques Garrigue (2004). "Relajando la restricción de valor" .

• Restricción de valor — MLton
• Notas sobre la restricción de valores de SML97 — Principios de los lenguajes de programación, Geoffrey Smith, Universidad Internacional de Florida