Алгоритм W и приведение мономорфного типа

Question

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

Вот выражения:

Expr ::= EAbs String Expr
       | EApp Expr Expr
       | EVar String
       | ELit
       | EConc Expr Expr

Правила ввода просты - мы переходим к использованию переменных типа для абстракции и применения. Вот все возможные типы:

Type ::= TVar String
       | TFun Type Type
       | TMono

Как вы уже догадались, ELit : TMono, и, более конкретно, EConc :: TMono → TMono → TMono,

Моя проблема возникает из-за фактического вывода типа. При повторении структуры выражения, общая техника при EAbs создать новую переменную типа, представляющую вновь связанную переменную, замените все случаи ввода в нашем контексте на (String : TVar fresh) суждение, а затем продолжить вниз по выражению.

Теперь, когда я ударил EConcЯ думал о том же подходе - замените переменные свободного выражения подвыражений на TMon в контексте введите вывод подвыражений и возьмите наиболее общий объединитель двух результатов в качестве основной подстановки для возврата. Тем не менее, когда я пытаюсь это с выражением, как EAbs "x" $ EConc ELit (EVar "x")Я ошибаюсь TFun (TVar "fresh") TMon,

Answer 1

Вам нужно использовать mgu принуждать подвыражения. Если вы напрямую манипулируете контекстом, чтобы влиять на подвыражения, вы не знаете, как это влияет на более ранние типы. использование mgu чтобы получить замену, которая объединяет подвыражения TMon, а затем составить эту замену в результате.