Вывод типов: алгоритм W

Элодий спустился из Подземья в Палату сверки с куском мела и пишет прямо на столе Лорры, между стопками контрактов. Тела контрактов Оракула написаны на Lisp из sexpr.py, том же маленьком языке, что и в первом этапе раздела. Твой тайпчекер из урока 86 знал только числа, логические значения и восемь операций:

print(typecheck(parse("(+ 1 (* 2 3))")))
print(typecheck(parse("(lambda (x) (+ x 1))")))

int
Traceback (most recent call last):
  File "/work/old_checker.py", line 5, in <module>
    print(typecheck(parse("(lambda (x) (+ x 1))")))
          ~~~~~~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/work/checker.py", line 55, in typecheck
    raise TypeMismatch(f"неизвестная операция: {to_string(head)}")
checker.TypeMismatch: неизвестная операция: lambda

Он считал снизу вверх: тип листьев известен, тип операции по таблице. Но у x в lambda листа с типом нет. Тип x надо угадать по тому, как его используют. Это вывод типов, и для таких языков, как Lisp Оракула, у него есть точный алгоритм с полувековой историей. Сегодня ты его соберёшь.