Зависимый МЛ

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

Зависимый ОД