Inferencia de tipos con sobrecarga

Question

Estoy trabajando en un sistema de tipos que admite la sobrecarga.Tengo una idea aproximada de cómo se implementa generalmente la inferencia de tipos en tal escenario, pero me pregunto cómo, una vez completada la inferencia de tipos, se puede elegir la implementación correcta de un operador sobrecargado.O, en otras palabras, cómo se puede pasar el tipo inferido al operador por el árbol de sintaxis.

Para un pequeño ejemplo, considere la expresión (x + y) + 1 dónde x :: N | S, y :: a, + :: (N -> N -> N) | (S -> S -> S), 1 :: N. :: representa tipo de, y a | b significa tipo a o tipo b.

La forma en que, supongo, funcionaría ahora la inferencia de tipos es atravesar el árbol de sintaxis y, para cada nodo, devolver una restricción de tipo:

(x + y) + 1 => ((N & (N[a=N] | S[a=S])), (N & N) -> N) | ((S & (N[a=N] | S[a=S])), (S & N) -> S) => N[a=N]
  1         => N
  +         => (N -> N -> N) | (S -> S -> S)
  x + y     => ((N & (N | S)), (N & a) -> N) | ((S & (N | S)), (S & a) -> S) => N[a=N] | S[a=S]
    x       => N | S
    y       => a
    +       => (N -> N -> N) | (S -> S -> S)

a & b en este ejemplo significa unificando los tipos a y b, [a=T, b=U] es un conjunto de restricciones de igualdad para variables de tipo.

Como era de esperar, el tipo de retorno de la expresión dada se infiere como N[a=N], eso es N donde la variable de tipo a se espera que sea N.

Por lo tanto, de las dos implementaciones proporcionadas para el + operador (N -> N -> N, S -> S -> S), N -> N -> N debería ser usado.En el ejemplo dado, se infiere el tipo resultante, pero no el tipo del operador sobrecargado.Mi pregunta es si existe un patrón común que se utiliza para informar al + nodo en el árbol de sintaxis de la implementación utilizada.

Answer 1

Podrías organizar la inferencia de tipos de la siguiente manera.

Supongamos que su sintaxis de entrada tiene tipo Input.Definir la sintaxis de salida Output ser como Input pero con anotaciones de tipo explícitas en todas las variables.La inferencia de tipos tendría tipo

infer : Input -> List (Output * Type)

Es decir, dada alguna información e, devuelve una lista de posibles respuestas.Cada respuesta es un par. (e', t) dónde e' es e con variables anotadas por tipos, y t es el tipo inferido de e.

Puedes ver esto como si todo esto estuviera sucediendo en la mónada de no determinismo.Siempre que necesites inferir el tipo de una variable x, buscas sus posibles tipos S | T | ... y ramificarse en cada uno de ellos.De esta manera no es necesario "devolver" ninguna información a las subexpresiones.En cambio, cada subexpresión ya viene anotada, de todas las formas posibles.