Inférence de type avec surcharge

Question

Je travaille sur un système de types prenant en charge la surcharge.J'ai une idée approximative de la façon dont l'inférence de type est généralement implémentée dans un tel scénario, mais je me demande comment - une fois l'inférence de type terminée - l'implémentation correcte d'un opérateur surchargé peut être choisie.Ou, en d’autres termes, comment le type déduit peut être retransmis à l’opérateur dans l’arborescence syntaxique.

Pour un petit exemple, considérons l'expression (x + y) + 1 où x :: N | S, y :: a, + :: (N -> N -> N) | (S -> S -> S), 1 :: N. :: représente Type de, et a | b représente le type a ou taper b.

La façon dont, je suppose, l'inférence de type fonctionnerait désormais consiste à parcourir l'arbre syntaxique et à renvoyer pour chaque nœud une contrainte de type :

(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 dans cet exemple signifie unificateur les genres a et b, [a=T, b=U] est un ensemble de contraintes d'égalité pour les variables de type.

Comme prévu, le type de retour de l'expression donnée est déduit comme N[a=N], c'est N où la variable de type a devrait être N.

Par conséquent, parmi les deux implémentations fournies pour le + opérateur (N -> N -> N, S -> S -> S), N -> N -> N Devrait être utilisé.Dans l’exemple donné, le type résultant est déduit, mais pas le type de l’opérateur surchargé.Ma question est de savoir s'il existe un modèle commun utilisé pour informer le + nœud dans l’arbre syntaxique de l’implémentation utilisée.

Answer 1

Vous pouvez organiser l'inférence de type comme suit.

Supposons que votre syntaxe d'entrée soit de type Input.Définir la syntaxe de sortie Output être comme Input mais avec des annotations de type explicites sur toutes les variables.L'inférence de type aurait le type

infer : Input -> List (Output * Type)

Autrement dit, compte tenu de certaines informations e, il renvoie une liste de réponses possibles.Chaque réponse est une paire (e', t) où e' est e avec des variables annotées par types, et t est le type déduit de e.

Vous pouvez voir tout cela comme se produisant dans la monade du non-déterminisme.Chaque fois que vous devez déduire le type d'une variable x, vous recherchez ses types possibles S | T | ... et branchez-vous sur chacun d'eux.De cette façon, vous n’avez pas à « renvoyer » d’informations aux sous-expressions.Au lieu de cela, chaque sous-expression est déjà annotée, de toutes les manières possibles.