Let-полиморфизм и Хиндли-Милнер: одна процедура на все улики

Агата Сомова · старший инспектор

Процедура «копия» берёт улику и возвращает её же. Ей всё равно, число это или «да/нет». Арбенина пользовалась ею в каждом втором деле, и в половине из них к разным уликам сразу. Если наш Допуск отказывает таким делам, значит, мы собрали не её Допуск. Найди, чего не хватает.

На столе папка, на которой вчера споткнулась унификация:

let copy = λx. x in if copy true then copy 0 else 0

Дело честное: оно вычисляется в 0 и нигде не застревает. Но ограничения из урока 55 требуют, чтобы у copy был один ярлык $X\to X$, а потом в одном месте X = Bool, в другом X = Nat. Конфликт.

Ошибка не в ограничениях, а в вопросе. Мы спрашивали «какой ярлык у копии». Правильный вопрос: «какой ярлык у копии в этом месте». Ответ на него дал Робин Милнер в 1978 году, а логик Роджер Хиндли пришёл к тому же раньше. Систему называют их именами: Хиндли-Милнер. На ней стоят ML, OCaml и Haskell, с которым ты работаешь с блока E.