Зависимый ML

Зависимый ML - экспериментальный предлагаемый язык функционального программирования Авторы: Хунвэй Си (Си 2007) и Фрэнк Пфеннинг. Зависимый ML расширяет ML за счет ограниченного понятия зависимых типов : типы могут зависеть от статических индексов типа Nat (натуральные числа ). Зависимое машинное обучение использует средство доказательства теорем об ограничениях, чтобы определить сильную эквациональную теорию по индексным выражениям.

Типы DML не зависят от значений времени выполнения - все еще существует различие фаз между компиляцией и выполнением программы. Ограничивая универсальность полностью зависимых типов, проверка типов остается разрешимой, но вывод типа становится неразрешимым.

Зависимое машинное обучение было заменено на ATS и больше не находится в активной разработке.

• Xi, Hongwei (март 2007 г.). «Зависимое машинное обучение: подход к практическому программированию с зависимыми типами» (PDF). Журнал функционального программирования. 17(2). CS1 maint: ref = harv (ссылка )
• и (2005). «Зависимые типы». В Пирс, Бенджамин С. (ред.) Расширенные темы по типам и языкам программирования. MIT Press.

• домашняя страница DML

.