Полагаю, я один из немногих, кто из первых рук узнал, почему это было сложно, поскольку я реализовал его в hbc, когда не было предшествующего уровня техники.
Итак, что было ясно из Wadler & BlottБумага заключалась в том, что проверка типов была расширением проверки типов Хиндли-Милнера и что во время выполнения вы должны передавать словари.От этого к реальной реализации довольно большой шаг.Хороший способ понять трудность состоит в том, чтобы фактически реализовать ее, начиная только с статьи Вадлера-Блотта.
Во-первых, вам нужно придумать идею средства проверки типов, которое не только проверяет типы, но и преобразовывает их.программа;вставка доказательств (словарей) при проверке типов.Вам также необходимо выяснить, как создавать новые словари из старых, используя объявления экземпляров в качестве системы логического вывода.
В ретроспективе это может показаться очевидным, но помните, что с тех пор многие работы с пояснениямибыло написано.Понимание того, как сделать что-то из бумаги, очень отличается от того, чтобы придумать это в первую очередь.
Кроме того, вы хотите, чтобы классы типов были достаточно эффективными, что приводит к собственному набору проблем.