Оглавление
Зависимый МЛ
-
Обзор DML
- DML – экспериментальный язык программирования, разработанный Хунвэем Си и Фрэнком Пфеннингом в 2007 году.
- Является диалектом ML, расширяет его за счет зависимых типов, зависящих от статических индексов типа Nat.
- Использует средство проверки теоремы об ограничениях для создания сильной уравнительной теории для индексных выражений.
- Типы DML не зависят от значений во время выполнения, что позволяет сохранить разрешимость проверки типов, но делает вывод типов неразрешимым.
- DML был заменен ATS и больше не разрабатывается активно.
-
Рекомендации и дополнительная информация
- Статья содержит ссылки на другие ресурсы, включая книгу “Зависимые типы” и фильм “Пирс, Бенджамин К.”, а также предлагает помощь в расширении статьи для Википедии.