Я пытаюсь написать свой собственный алгоритм вывода типа для игрушечного языка, но я сталкиваюсь с стеной - я думаю, что алгоритм W может использоваться только для чрезмерно общих типов.Алгоритм 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
.
Я не уверен, что манипулирование контекстом - правильный подход. Может быть, взять самый общий унификатор незакрытых подвыражений с помощью 'TMon'? –