Алгоритм 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, а затем создайте эту замену в результате.