Sistema tipo Hindley-Milner

En el cálculo lambda de tipos simples , los tipos T son constantes de tipo atómico o tipos de función de la forma${\displaystyle T\rightarrow T}$Estos tipos son monomórficos . Ejemplos típicos son los tipos utilizados en valores aritméticos:

${\displaystyle {\begin{array}{ll}3&:{\mathtt {Número}}\\{\mathtt {sumar}}\ 3\ 4&:{\mathtt {Número}}\\{\mathtt {sumar}}&:{\mathtt {Número}}\rightarrow {\mathtt {Número}}\rightarrow {\mathtt {Número}}\end{array}}}$

Por el contrario, el cálculo lambda sin tipado es completamente neutral respecto al tipado, y muchas de sus funciones pueden aplicarse de forma significativa a cualquier tipo de argumento. El ejemplo más sencillo es la función identidad.

${\displaystyle {\mathtt {id}}\equiv \lambda xx}$

que simplemente devuelve cualquier valor al que se aplique. Ejemplos menos triviales incluyen tipos paramétricos como las listas .

Si bien el polimorfismo en general implica que las operaciones aceptan valores de más de un tipo, el polimorfismo utilizado aquí es paramétrico. En la literatura también se encuentra la notación de esquemas de tipos , que enfatiza la naturaleza paramétrica del polimorfismo. Además, las constantes pueden tipificarse con variables de tipo (cuantificadas). Por ejemplo, los siguientes esquemas de tipos cuantifican universalmente sobre${\displaystyle \alpha }$, lo que significa que son ciertas para todas las posibles${\displaystyle \alpha }$:

${\displaystyle {\begin{array}{ll}{\mathtt {cons}}&:\forall \alpha .\alpha \rightarrow {\mathtt {List}}\ \alpha \rightarrow {\mathtt {List}}\ \alpha \\{\mathtt {nil}}&:\forall \alpha .{\mathtt {List}}\ \alpha \\{\mathtt {id}}&:\forall \alpha .\alpha \rightarrow \alpha \end{array}}}$

Los tipos polimórficos pueden convertirse en monomórficos mediante la sustitución consistente de sus variables. Ejemplos de instancias monomórficas son:

${\displaystyle {\begin{array}{ll}{\mathtt {id}}'&:{\mathtt {String}}\rightarrow {\mathtt {String}}\\{\mathtt {nil}}'&:{\mathtt {List}}\ {\mathtt {Number}}\end{array}}}$

En términos más generales, los tipos son polimórficos cuando contienen variables de tipo, mientras que los tipos que no las contienen son monomórficos.

A diferencia de los sistemas de tipos utilizados, por ejemplo, en Pascal (1970) o C (1972), que solo admiten tipos monomórficos, HM está diseñado con énfasis en el polimorfismo paramétrico. Los sucesores de los lenguajes mencionados, como C++ (1985), se centraron en diferentes tipos de polimorfismo, concretamente el subtipado en relación con la programación orientada a objetos y la sobrecarga . Si bien el subtipado es incompatible con HM, existe una variante de sobrecarga sistemática disponible en el sistema de tipos de Haskell, basado en HM.

Al extender la inferencia de tipos para el cálculo lambda de tipos simples hacia el polimorfismo, hay que decidir si es admisible asignar un tipo polimórfico no solo como tipo de una expresión, sino también como tipo de una variable ligada a λ. Esto permitiría asignar el tipo genérico identidad a la variable 'id' en:

(λ id . ... (id 3) ... (id "texto") ... ) (λ x . x)

Permitir esto da lugar al cálculo lambda polimórfico ; sin embargo, la inferencia de tipos en este sistema no es decidible. ^{[ 5 ]} En cambio, HM distingue las variables que están inmediatamente ligadas a una expresión de las variables ligadas a λ más generales, llamando a las primeras variables ligadas a let, y permite que se asignen tipos polimórficos solo a estas. Esto lleva al polimorfismo let donde el ejemplo anterior toma la forma

sea ​​id = λ x . x en ... (id 3) ... (id "texto") ...

que se puede tipificar con un tipo polimórfico para 'id'. Como se indicó, la sintaxis de la expresión se extiende para hacer explícitas las variables ligadas a let, y al restringir el sistema de tipos para permitir que solo las variables ligadas a let tengan tipos polimórficos, mientras que los parámetros en las abstracciones lambda deben obtener un tipo monomórfico, la inferencia de tipos se vuelve decidible.

Las expresiones que se deben escribir son exactamente las del cálculo lambda extendido con una expresión let, como se muestra en la tabla adjunta. Se pueden usar paréntesis para desambiguar una expresión. La aplicación es de enlace izquierdo y enlaza con mayor fuerza que la abstracción o la construcción let-in.

Los tipos se dividen sintácticamente en dos grupos: monotipos y politipos. ^{[ nota 2 ]}

El polimorfismo implica que una misma expresión puede tener (quizás infinitas) variantes. Sin embargo, en este sistema de tipos, estas variantes no son completamente independientes, sino que están condicionadas por el polimorfismo paramétrico.

Como ejemplo, la identidad${\displaystyle \lambda x.x}$puede tener${\displaystyle \forall \alpha .\alpha \rightarrow \alpha }$como su tipo así como ${\displaystyle {\texttt {string}}\rightarrow {\texttt {string}}}$o${\displaystyle {\texttt {int}}\rightarrow {\texttt {int}}}$y muchos otros, pero no${\displaystyle {\texttt {int}}\rightarrow {\texttt {string}}}$. El tipo más general para esta función es ${\displaystyle \forall \alpha .\alpha \rightarrow \alpha }$, mientras que los demás son más específicos y pueden derivarse del general reemplazando consistentemente otro tipo por el parámetro de tipo , es decir, la variable cuantificada${\displaystyle \alpha }$El contraejemplo falla porque la sustitución no es consistente.

La sustitución consistente puede formalizarse aplicando una sustitución.${\displaystyle S=\left\{\ a_{i}\mapsto \tau _{i},\ \dots \ \right\}}$al término de un tipo${\displaystyle \tau }$, escrito${\displaystyle S\tau }$Como sugiere el ejemplo, la sustitución no solo está fuertemente relacionada con un orden, que expresa que un tipo es más o menos especial, sino también con la cuantificación total que permite que se aplique la sustitución.

Formalmente, en HM, un tipo${\displaystyle \sigma '}$es más general que${\displaystyle \sigma }$formalmente${\displaystyle \sigma '\sqsubseteq \sigma }$, si alguna variable cuantificada en${\displaystyle \sigma '}$se sustituye de forma consistente de tal manera que se obtiene${\displaystyle \sigma }$como se muestra en la barra lateral. Este orden forma parte de la definición de tipo del sistema de tipos.

En nuestro ejemplo anterior, aplicando la sustitución${\displaystyle S=\left\{\alpha \mapsto {\texttt {string}}\right\}}$resultaría en${\displaystyle \forall \alpha .\alpha \rightarrow \alpha \sqsubseteq {\texttt {string}}\rightarrow {\texttt {string}}}$.

Si bien sustituir un tipo monomórfico (base) por una variable cuantificada es sencillo, sustituir un politipo presenta algunas dificultades debido a la presencia de variables libres. En particular, las variables no ligadas no deben reemplazarse, ya que se tratan como constantes. Además, las cuantificaciones solo pueden ocurrir en el nivel superior. Al sustituir un tipo paramétrico, es necesario elevar sus cuantificadores. La tabla de la derecha aclara esta regla.

Como alternativa, consideremos una notación equivalente para los politipos sin cuantificadores, en la que las variables cuantificadas se representan mediante un conjunto diferente de símbolos. En dicha notación, la especialización se reduce a una simple sustitución consistente de dichas variables.

La relación${\displaystyle \sqsubseteq }$es un pedido parcial y ${\displaystyle \forall \alpha .\alpha }$es su elemento más pequeño.

La sintaxis de HM se traslada a la sintaxis de las reglas de inferencia que conforman el cuerpo del sistema formal , utilizando los tipos como juicios . Cada regla define qué conclusión se puede extraer de qué premisas. Además de los juicios, algunas condiciones adicionales introducidas anteriormente también pueden utilizarse como premisas.

Una demostración que utiliza las reglas es una secuencia de juicios tal que todas las premisas se enumeran antes de una conclusión. Los ejemplos a continuación muestran un posible formato de demostraciones. De izquierda a derecha, cada línea muestra la conclusión, la${\displaystyle [{\mathtt {Name}}]}$de la regla aplicada y las premisas, ya sea haciendo referencia a una línea (número) anterior si la premisa es un juicio o haciendo explícito el predicado.

Aunque no es visible de inmediato, el conjunto de reglas codifica una regulación bajo la cual un tipo puede generalizarse o no mediante un uso ligeramente variable de monotipos y politipos en las reglas.${\displaystyle [{\mathtt {Abs}}]}$y${\displaystyle [{\mathtt {Let}}]}$Recuerda que${\displaystyle \sigma }$y${\displaystyle \tau }$denotan poli- y monotipos respectivamente.

En regla${\displaystyle [{\mathtt {Abs}}]}$, el valor variable del parámetro de la función${\displaystyle \lambda x.e}$se agrega al contexto con un tipo monomórfico a través de la premisa${\displaystyle \Gamma ,\ x:\tau \vdash _{D}e:\tau '}$, mientras que en la regla ${\displaystyle [{\mathtt {Let}}]}$La variable ingresa al entorno en forma polimórfica.${\displaystyle \Gamma ,\ x:\sigma \vdash _{D}e_{1}:\tau }$. Aunque en ambos casos la presencia de${\displaystyle x}$En este contexto, se impide el uso de la regla de generalización para cualquier variable libre en la asignación; esta regulación impone el tipo de parámetro.${\displaystyle x}$en un${\displaystyle \lambda }$-la expresión debe permanecer monomórfica, mientras que en una expresión let, la variable podría introducirse de forma polimórfica, lo que posibilita las especializaciones.

Como consecuencia de esta regulación,${\displaystyle \lambda f.(f\,{\textrm {true}},f\,{\textrm {0}})}$no se puede tipificar, ya que el parámetro${\displaystyle f}$está en una posición monomórfica, mientras que${\displaystyle {\textbf {let}}\ f=\lambda x.x\,{\textbf {in}}\,(f\,{\textrm {true}},f\,{\textrm {0}})}$tiene tipo${\displaystyle (bool,int)}$, porque${\displaystyle f}$se ha introducido en una expresión let y, por lo tanto, se trata como polimórfica.

La regla de generalización también merece un análisis más detallado. Aquí, la cuantificación total implícita en la premisa${\displaystyle \Gamma \vdash _{D}e:\sigma }$simplemente se mueve al lado derecho de${\displaystyle \vdash _{D}}$en la conclusión, limitada por un cuantificador universal explícito. Esto es posible, ya que${\displaystyle \alpha }$No se produce de forma espontánea en este contexto. De nuevo, si bien esto hace plausible la regla de generalización, no es realmente una consecuencia. Por el contrario, la regla de generalización forma parte de la definición del sistema de tipos de HM y la cuantificación total implícita es una consecuencia.

Aislando los puntos en una prueba, donde no es posible ninguna decisión, el primer grupo de reglas centrado en la sintaxis no deja elección ya que a cada regla sintáctica le corresponde una regla de tipificación única, que determina una parte de la prueba, mientras que entre la conclusión y las premisas de estas partes fijas existen cadenas de${\displaystyle [{\mathtt {Inst}}]}$y${\displaystyle [{\mathtt {Gen}}]}$ Podría ocurrir. Tal cadena también podría existir entre la conclusión de la demostración y la regla para la expresión superior. Todas las demostraciones deben tener la forma esbozada.

Porque la única opción en una prueba con respecto a la selección de reglas son las ${\displaystyle [{\mathtt {Inst}}]}$y${\displaystyle [{\mathtt {Gen}}]}$En cuanto a las cadenas, la forma de la prueba plantea la cuestión de si se puede precisar aún más, de modo que dichas cadenas no sean necesarias. De hecho, esto es posible y da lugar a una variante del sistema de reglas sin tales reglas.

Un tratamiento contemporáneo de HM utiliza un sistema de reglas puramente dirigido por la sintaxis debido a Clement ^{[ 6 ]} como paso intermedio. En este sistema, la especialización se ubica directamente después de la original.${\displaystyle [{\mathtt {Var}}]}$regla y se fusionó con ella, mientras que la generalización pasa a formar parte de la${\displaystyle [{\mathtt {Let}}]}$regla. Allí también se determina que la generalización siempre produzca el tipo más general mediante la introducción de la función.${\displaystyle {\bar {\Gamma }}(\tau )}$, que cuantifica todas las variables monotipo no ligadas en${\displaystyle \Gamma }$.

Formalmente, para validar que este nuevo sistema de reglas${\displaystyle \vdash _{S}}$es equivalente al original${\displaystyle \vdash _{D}}$, uno tiene que demostrar que${\displaystyle \Gamma \vdash _{D}\ e:\sigma \Leftrightarrow \Gamma \vdash _{S}\ e:\sigma }$, que se descompone en dos subpruebas:

• ${\displaystyle \Gamma \vdash _{D}\ e:\sigma \Leftarrow \Gamma \vdash _{S}\ e:\sigma }$( Consistencia )
• ${\displaystyle \Gamma \vdash _{D}\ e:\sigma \Rightarrow \Gamma \vdash _{S}\ e:\sigma }$( Integridad )

Si bien la coherencia se puede observar descomponiendo las reglas${\displaystyle [{\mathtt {Let}}]}$y${\displaystyle [{\mathtt {Var}}]}$ de${\displaystyle \vdash _{S}}$en pruebas en${\displaystyle \vdash _{D}}$, es probable que sea visible que${\displaystyle \vdash _{S}}$está incompleto, ya que no se puede demostrar${\displaystyle \lambda \ x.x:\forall \alpha .\alpha \rightarrow \alpha }$en${\displaystyle \vdash _{S}}$, por ejemplo, pero solo ${\displaystyle \lambda \ x.x:\alpha \rightarrow \alpha }$Sin embargo , se puede demostrar una versión ligeramente más débil de completitud ^{[ 7 ]} , a saber:

• ${\displaystyle \Gamma \vdash _{D}\ e:\sigma \Rightarrow \Gamma \vdash _{S}\ e:\tau \wedge {\bar {\Gamma }}(\tau )\sqsubseteq \sigma }$

lo que implica que se puede derivar el tipo principal para una expresión en${\displaystyle \vdash _{S}}$lo que nos permite generalizar la demostración al final.

Comparando${\displaystyle \vdash _{D}}$y${\displaystyle \vdash _{S}}$Ahora, solo aparecen monotipos en los juicios de todas las reglas. Además, la forma de cualquier prueba posible con el sistema de deducción es ahora idéntica a la forma de la expresión (ambas vistas como árboles ). Por lo tanto, la expresión determina completamente la forma de la prueba. En${\displaystyle \vdash _{D}}$La forma probablemente se determinaría con respecto a todas las reglas excepto${\displaystyle [{\mathtt {Inst}}]}$y${\displaystyle [{\mathtt {Gen}}]}$, que permiten construir ramas (cadenas) de longitud arbitraria entre los demás nodos.

Ahora que se conoce la estructura de la prueba, ya se está cerca de formular un algoritmo de inferencia de tipos. Dado que cualquier prueba para una expresión dada debe tener la misma estructura, se puede asumir que los monotipos en los juicios de la prueba son indeterminados y considerar cómo determinarlos.

Aquí entra en juego el orden de sustitución (especialización). Aunque a primera vista no se pueden determinar los tipos localmente, se espera que sea posible refinarlos con la ayuda del orden mientras se recorre el árbol de prueba, asumiendo además, dado que el algoritmo resultante se convertirá en un método de inferencia, que el tipo en cualquier premisa se determinará como el mejor posible. Y de hecho, se puede, como se observa en las reglas de${\displaystyle \vdash _{S}}$sugiere:

• [ Abs ] : La elección crítica es τ . En este punto, no se sabe nada sobre τ , por lo que solo se puede asumir el tipo más general, que es${\displaystyle \forall \alpha .\alpha }$El plan consiste en especializar el tipo si fuera necesario. No se permite un politipo en este caso, así que por ahora tendremos que usar algún α . Para evitar capturas no deseadas, una variable de tipo que aún no esté en la prueba es una opción segura. Además, hay que tener en cuenta que este monotipo aún no está fijo, sino que podría refinarse posteriormente.
• [ Var ] : La elección radica en cómo refinar σ . Dado que cualquier elección de un tipo τ aquí depende del uso de la variable, que no se conoce localmente, la opción más segura es la más general. Utilizando el mismo método anterior, se pueden instanciar todas las variables cuantificadas en σ con nuevas variables monotipo, manteniéndolas así abiertas a un mayor refinamiento.
• [ Let ] : La regla no deja otra opción. Hecho.
• [ Aplicación ] : Solo la regla de aplicación podría forzar un refinamiento de las variables "abiertas" hasta el momento, como lo requieren ambas premisas.
  1. La primera premisa obliga a que el resultado de la inferencia sea de la forma${\displaystyle \tau \rightarrow \tau '}$.
     • Si es así, perfecto. Después se puede elegir su τ ' para el resultado.
     • De lo contrario, podría tratarse de una variable abierta. En ese caso, se puede refinar a la forma requerida con dos nuevas variables, como antes.
     • De lo contrario, la comprobación de tipos falla porque la primera premisa infirió un tipo que no es ni puede convertirse en un tipo de función .
  2. La segunda premisa exige que el tipo inferido sea igual a τ de la primera premisa. Ahora disponemos de dos tipos posiblemente diferentes, quizás con variables de tipo abiertas, para comparar e igualar si es posible. Si lo es, se encuentra una mejora; de lo contrario, se detecta un error de tipo. Se conoce un método eficaz para "igualar dos términos" mediante sustitución: la Unificación de Robinson en combinación con el algoritmo Union-Find .

Para resumir brevemente el algoritmo de unión-búsqueda, dado el conjunto de todos los tipos en una prueba, permite agruparlos en clases de equivalencia mediante un procedimiento de unión y elegir un representante para cada una de dichas clases utilizando un procedimiento de búsqueda . Haciendo hincapié en la palabra procedimiento en el sentido de efecto secundario , claramente estamos abandonando el ámbito de la lógica para preparar un algoritmo eficaz. El representante de una${\displaystyle {\mathtt {union}}(a,b)}$se determina de tal manera que, si tanto a como b son variables de tipo, entonces el representante es arbitrariamente uno de ellos, pero al unir una variable y un término, el término se convierte en el representante. Suponiendo que se dispone de una implementación de unión-búsqueda, se puede formular la unificación de dos monotipos de la siguiente manera:

unificar(ta, tb): ta = encontrar(ta) tb = encontrar(tb) si ambos ta,tb son términos de la forma D p1..pn con D,n idénticos entonces unify(ta[i], tb[i]) para cada parámetro i correspondiente sino si al menos uno de ta,tb es una variable de tipo entonces unión(ta, tb) De lo contrario, se producirá el error 'los tipos no coinciden'.

Ahora que tenemos un esbozo de un algoritmo de inferencia, se ofrece una presentación más formal en la siguiente sección. Se describe en Milner ^{[ 2 ]} P. 370 y ss. como algoritmo J.

La presentación del Algoritmo J es un mal uso de la notación de reglas lógicas, ya que incluye efectos secundarios pero permite una comparación directa con${\displaystyle \vdash _{S}}$al tiempo que se expresa una implementación eficiente. Las reglas ahora especifican un procedimiento con parámetros${\displaystyle \Gamma ,e}$flexible${\displaystyle \tau }$en la conclusión donde la ejecución de las premisas procede de izquierda a derecha.

El procedimiento${\displaystyle inst(\sigma )}$especializa el politipo${\displaystyle \sigma }$copiando el término y reemplazando consistentemente las variables de tipo ligado por nuevas variables monotype.${\displaystyle newvar}$' produce una nueva variable monotipo. Probablemente,${\displaystyle {\bar {\Gamma }}(\tau )}$tiene que copiar el tipo introduciendo nuevas variables para la cuantificación para evitar capturas no deseadas. En general, el algoritmo ahora procede haciendo siempre la elección más general dejando la especialización a la unificación, que por sí misma produce el resultado más general. Como se señaló anteriormente , el resultado final${\displaystyle \tau }$tiene que generalizarse a${\displaystyle {\bar {\Gamma }}(\tau )}$al final, para obtener el tipo más general para una expresión dada.

Debido a que los procedimientos utilizados en el algoritmo tienen un costo cercano a O(1), el costo total del algoritmo es casi lineal con respecto al tamaño de la expresión para la cual se debe inferir un tipo. Esto contrasta notablemente con muchos otros intentos de desarrollar algoritmos de inferencia de tipos, que a menudo resultaron ser NP-difíciles , o incluso indecidibles con respecto a la terminación. Por lo tanto, el algoritmo HM se desempeña tan bien como los mejores algoritmos de verificación de tipos completamente informados. En este contexto, la verificación de tipos significa que un algoritmo no tiene que encontrar una prueba, sino solo validar una ya dada.

La eficiencia se reduce ligeramente porque se debe mantener la vinculación de las variables de tipo en el contexto para permitir el cálculo de${\displaystyle {\bar {\Gamma }}(\tau )}$y habilitar una comprobación de ocurrencias para evitar la creación de tipos recursivos durante${\displaystyle {\mathit {unify}}(\alpha ,\tau )}$Un ejemplo de tal caso es${\displaystyle \lambda \ x.(x\ x)}$, para los cuales no se puede derivar ningún tipo usando HM. En la práctica, los tipos son solo términos pequeños y no construyen estructuras expansivas. Por lo tanto, en el análisis de complejidad, se puede tratar su comparación como una constante, manteniendo costos O(1).

A partir de ahí, una demostración del algoritmo J conduce al algoritmo W, que solo produce los efectos secundarios impuestos por el procedimiento.${\displaystyle {\textit {union}}}$explícito al expresar su composición serial por medio de las sustituciones ${\displaystyle S_{i}}$. La presentación del algoritmo W en la barra lateral todavía utiliza efectos secundarios en las operaciones establecidas en cursiva, pero estos ahora se limitan a generar nuevos símbolos. La forma de juicio es${\displaystyle \Gamma \vdash e:\tau ,S}$, que denota una función con un contexto y una expresión como parámetro que produce un monotipo junto con una sustitución.${\displaystyle {\textsf {mgu}}}$es una versión sin efectos secundarios de${\displaystyle {\textit {union}}}$produciendo una sustitución que es el unificador más general .

Si bien el algoritmo W normalmente se considera el algoritmo HM y a menudo se presenta directamente después del sistema de reglas en la literatura, su propósito es descrito por Milner ^{[ 2 ]} en la página 369 de la siguiente manera:

Tal como está, W no es un algoritmo eficiente; se aplican sustituciones con demasiada frecuencia. Fue formulado para facilitar la demostración de su corrección. Ahora presentamos un algoritmo J más simple que simula W de forma precisa.

Si bien consideraba que W era más complejo y menos eficiente, lo presentó en su publicación antes que J. Tiene sus ventajas cuando los efectos secundarios no están disponibles o son indeseados. W también es necesario para demostrar la completitud, lo cual él considera parte de la prueba de solidez.

Antes de formular las obligaciones de prueba, es necesario destacar una diferencia entre los sistemas de reglas D y S y los algoritmos presentados.

Si bien el desarrollo anterior hizo un uso indebido de los monotipos como variables de prueba "abiertas", se evitó la posibilidad de que las variables monotípicas adecuadas se vieran afectadas introduciendo nuevas variables y esperando que todo saliera bien. Pero hay un inconveniente: una de las promesas era que estas nuevas variables se "tendrían en cuenta" como tales. El algoritmo no cumple con esta promesa.

Tener un contexto${\displaystyle 1:int,\ f:\alpha }$, la expresión${\displaystyle f\ 1}$ tampoco se puede escribir${\displaystyle \vdash _{D}}$o${\displaystyle \vdash _{S}}$, pero los algoritmos dan con el tipo${\displaystyle \beta }$, donde W además proporciona la sustitución${\displaystyle \left\{\alpha \mapsto int\rightarrow \beta \right\}}$Esto significa que el algoritmo no detecta todos los errores de tipo. Esta omisión se puede solucionar fácilmente distinguiendo con mayor precisión entre variables de prueba y variables monotipo.

Los autores eran plenamente conscientes del problema, pero decidieron no solucionarlo. Se podría suponer que existe una razón pragmática detrás de esto. Si bien una implementación más adecuada de la inferencia de tipos habría permitido que el algoritmo manejara monotipos abstractos, estos no eran necesarios para la aplicación prevista, donde ninguno de los elementos en un contexto preexistente tiene variables libres. En este sentido, se eliminó la complicación innecesaria en favor de un algoritmo más simple. La desventaja restante es que la prueba del algoritmo con respecto al sistema de reglas es menos general y solo se puede realizar para contextos con${\displaystyle free(\Gamma )=\emptyset }$como condición adicional.

${\displaystyle {\begin{array}{lll}{\text{(Correctness)}}&\Gamma \vdash _{W}e:\tau ,S&\quad \Longrightarrow \quad \Gamma \vdash _{S}e:\tau \\{\text{(Completeness)}}&\Gamma \vdash _{S}e:\tau &\quad \Longrightarrow \quad \Gamma \vdash _{W}e:\tau ',S\quad \quad {\text{forall}}\ \tau \ {\text{where}}\ {\overline {\emptyset }}(\tau ')\sqsubseteq \tau \end{array}}}$

La condición adicional en la obligación de completitud aborda cómo la deducción puede generar muchos tipos, mientras que el algoritmo siempre produce uno. Al mismo tiempo, la condición adicional exige que el tipo inferido sea realmente el más general.

Para probar adecuadamente las obligaciones, primero es necesario fortalecerlas para permitir la activación del lema de sustitución que enlaza la sustitución.${\displaystyle S}$a través de${\displaystyle \vdash _{S}}$y${\displaystyle \vdash _{W}}$. A partir de ahí, las demostraciones se realizan por inducción sobre la expresión.

Otra obligación de prueba es el lema de sustitución en sí, es decir, la sustitución de la tipificación, que finalmente establece la cuantificación total. Esto último no puede probarse formalmente, ya que no se dispone de dicha sintaxis.

Para que la programación sea práctica, se necesitan funciones recursivas. Una propiedad fundamental del cálculo lambda es que las definiciones recursivas no están disponibles directamente, sino que pueden expresarse mediante un combinador de punto fijo . Sin embargo, el combinador de punto fijo no puede formularse en una versión tipada del cálculo lambda sin que ello tenga un efecto desastroso en el sistema, como se explica a continuación.

La sobrecarga implica que se pueden definir y usar diferentes funciones con el mismo nombre. La mayoría de los lenguajes de programación, al menos, ofrecen sobrecarga con las operaciones aritméticas integradas (+, <, etc.), lo que permite al programador escribir expresiones aritméticas de la misma forma, incluso para diferentes tipos numéricos como into real. Dado que la combinación de estos diferentes tipos dentro de la misma expresión también requiere una conversión implícita, la sobrecarga, especialmente para estas operaciones, suele estar integrada en el propio lenguaje de programación. En algunos lenguajes, esta característica se generaliza y se pone a disposición del usuario, por ejemplo, en C++.

Si bien en la programación funcional se ha evitado la sobrecarga ad hoc debido a los costos computacionales tanto en la verificación de tipos como en la inferencia , se ha introducido un método para sistematizar la sobrecarga que se asemeja, tanto en forma como en nomenclatura, a la programación orientada a objetos, pero que opera un nivel superior. En este sistema, las "instancias" no son objetos (es decir, a nivel de valor), sino tipos. El ejemplo de ordenación rápida mencionado en la introducción utiliza la sobrecarga en los órdenes, con la siguiente anotación de tipo en Haskell:

Ordenar rápido :: Orden a => [ a ] ​​-> [ a ]

En este caso, el tipo ano solo es polimórfico, sino que también está restringido a ser una instancia de alguna clase de tipo Ordque proporciona los predicados de ordenación <utilizados >=en el cuerpo de las funciones. Las implementaciones adecuadas de estos predicados se pasan a quicksort como parámetros adicionales, tan pronto como quicksort se utiliza en tipos más concretos que proporcionan una única implementación de la función sobrecargada quickSort.

Dado que las "clases" solo admiten un único tipo como argumento, el sistema de tipos resultante aún puede proporcionar inferencia. Además, las clases de tipos pueden equiparse con algún tipo de orden de sobrecarga que permite organizar las clases como un retículo .

El polimorfismo paramétrico implica que los tipos se pasan como parámetros, como si fueran valores propios. Al pasarlos como argumentos a funciones propias, pero también a funciones de tipo (como en las constantes de tipo paramétricas), surge la pregunta de cómo tipificar los tipos de forma más precisa. Los tipos de orden superior se utilizan para crear un sistema de tipos aún más expresivo.

La unificación ya no es decidible en presencia de metatipos, lo que imposibilita la inferencia de tipos en este grado de generalidad. Además, asumir un tipo de todos los tipos que se incluya a sí mismo como tipo conduce a una paradoja, como en el conjunto de todos los conjuntos, por lo que es necesario proceder por niveles de abstracción. La investigación en cálculo lambda de segundo orden , un nivel superior, demostró que la inferencia de tipos es indecidible en este grado de generalidad.

Haskell introduce un nivel superior llamado tipo . En Haskell estándar, los tipos se infieren y se utilizan para poco más que describir la aridad de los constructores de tipos. Por ejemplo, se piensa que un constructor de tipo de lista mapea un tipo (el tipo de sus elementos) a otro tipo (el tipo de la lista que contiene dichos elementos); notacionalmente esto se expresa como${\displaystyle *\to *}$. Existen extensiones de lenguaje que extienden los tipos para emular características de un sistema de tipos dependiente . ^{[ 8 ]}

Los intentos de combinar la subtipificación y la inferencia de tipos han causado bastante frustración. Es sencillo acumular y propagar restricciones de subtipificación (a diferencia de las restricciones de igualdad de tipos), haciendo que las restricciones resultantes formen parte de los esquemas de tipificación inferidos, por ejemplo${\displaystyle \forall \alpha .\ (\alpha \leq T)\Rightarrow \alpha \rightarrow \alpha }$, dónde${\displaystyle \alpha \leq T}$es una restricción en la variable de tipo${\displaystyle \alpha }$Sin embargo, debido a que las variables de tipo ya no se unifican de manera entusiasta en este enfoque, tiende a generar esquemas de tipado grandes y difíciles de manejar que contienen muchas variables de tipo y restricciones inútiles, lo que los hace difíciles de leer y comprender. Por lo tanto, se dedicó un esfuerzo considerable a simplificar dichos esquemas de tipado y sus restricciones, utilizando técnicas similares a las de la simplificación de autómatas finitos no deterministas (NFA) (útiles en presencia de tipos recursivos inferidos). ^{[ 9 ]} Más recientemente, Dolan y Mycroft ^{[ 10 ]} formalizaron la relación entre la simplificación del esquema de tipado y la simplificación de NFA y demostraron que una toma algebraica de la formalización del subtipado permitía generar esquemas de tipado principales compactos para un lenguaje similar a ML (llamado MLsub). En particular, su esquema de tipado propuesto utilizaba una forma restringida de tipos de unión e intersección en lugar de restricciones explícitas. Parreaux afirmó posteriormente ^{[ 11 ]} que esta formulación algebraica era equivalente a un algoritmo relativamente simple parecido al Algoritmo W, y que el uso de tipos de unión e intersección no era esencial.

Por otro lado, la inferencia de tipos ha demostrado ser más difícil en el contexto de los lenguajes de programación orientados a objetos, porque los métodos de objetos tienden a requerir polimorfismo de primera clase al estilo del Sistema F (donde la inferencia de tipos es indecidible) y debido a características como el polimorfismo acotado por F. En consecuencia, los sistemas de tipos con subtipos que permiten la programación orientada a objetos, como el sistema de Cardelli${\displaystyle F_{<:}}$, ^{[ 12 ]} no admiten la inferencia de tipo estilo HM.

El polimorfismo de filas puede utilizarse como alternativa al subtipado para admitir características del lenguaje como los registros estructurales. ^{[ 13 ]} Si bien este estilo de polimorfismo es menos flexible que el subtipado en algunos aspectos, en particular al requerir más polimorfismo del estrictamente necesario para lidiar con la falta de direccionalidad en las restricciones de tipo, tiene la ventaja de que puede integrarse con los algoritmos HM estándar con bastante facilidad.