Реализация алгоритма вывода типа Дамаса-Хиндли-Милнера

Question

Я ищу информацию об известном алгоритме Дамаса-Хиндли-Милнера для определения типа для функциональных языков, особенно информацию о реализации.

Я уже знаю, каксделать алгоритм W , но я слышал о недавних новых алгоритмах, основанных на генераторе / решателе ограничений, а не на обычной унификации.Однако мне не удается найти какие-либо дискуссии о реализации этого нового алгоритма.

Есть идеи, где я мог бы найти некоторую частичную информацию о выводе ML?

Answer 1

Если вы знакомы с ML-кодом, лучший способ найти эти вещи - просто взглянуть на реализации в дикой природе. Хорошая эталонная реализация - HaMLet , которая предназначена скорее как тестовая платформа, чем как производственная реализация.

Почти все серьезное недавнее обсуждение этих вопросов будет происходить в научных кругах. Одна статья, которая может быть интересна: Обобщающие алгоритмы вывода типа Хиндли-Милнера .

Кроме того, реализации систем различных типов (в том числе полиморфизма let) в « Типах и языках программирования» Пирса », а также в« Современный реализации компилятора »в ML от Appel соответствовать современным подходам к реализации этого, чем ванильное описание алгоритма W.