Вывод типа с перегрузкой

Question

Я работаю над системой типов, поддерживающей перегрузку.У меня есть приблизительное представление о том, как обычно реализуется вывод типа в таком сценарии, но мне интересно, как - после завершения вывода типа - можно выбрать правильную реализацию перегруженного оператора.Или, другими словами, как выведенный тип может быть передан обратно по синтаксическому дереву оператору.

Для небольшого примера рассмотрим выражение (x + y) + 1 где x :: N | S, y :: a, + :: (N -> N -> N) | (S -> S -> S), 1 :: N. :: расшифровывается как тип, и a | b расшифровывается как тип a или Тип b.

Я предполагаю, что теперь будет работать вывод типа, заключающийся в том, чтобы пройти по синтаксическому дереву и для каждого узла вернуть ограничение типа:

(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 в этом примере расшифровывается как объединяющий типы a и b, [a=T, b=U] представляет собой набор ограничений равенства для переменных типа.

Как и ожидалось, возвращаемый тип данного выражения выводится как N[a=N], то есть N где переменная типа a ожидается, что будет N.

Таким образом, из двух предоставленных реализаций для + оператор (N -> N -> N, S -> S -> S), N -> N -> N должен быть использован.В приведенном примере выводится результирующий тип, но не тип перегруженного оператора.Мой вопрос заключается в том, существует ли общий шаблон, который используется для информирования + узел в синтаксическом дереве используемой реализации.

Answer 1

Вы могли бы организовать вывод типа следующим образом.

Предположим, что ваш синтаксис ввода имеет тип Input.Определите синтаксис вывода Output быть похожим Input но с явными аннотациями типов для всех переменных.Вывод типа будет иметь тип

infer : Input -> List (Output * Type)

То есть, учитывая некоторые входные данные e, он возвращает список возможных ответов.Каждый ответ представляет собой пару (e', t) где e' является e с переменными, аннотированными по типам, и t является предполагаемым типом e.

Вы можете рассматривать все это как происходящее в монаде недетерминизма.Всякий раз, когда вам нужно определить тип переменной x, вы просматриваете его возможные типы S | T | ... и разветвляйтесь на каждом из них.Таким образом, вам не нужно "передавать обратно" какую-либо информацию во вложенные выражения.Вместо этого каждое вложенное выражение уже снабжено комментариями всеми возможными способами.