Зависимый ОД

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

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

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

Дальнейшее чтение

• Си Цзиньпин, Хунвэй (март 2007 г.). «Зависимое машинное обучение: подход к практическому программированию с зависимыми типами» . Журнал функционального программирования . 17 (2): 215–286. дои : 10.1017/S0956796806006216 . S2CID   45996427 .
• Дэвид Аспиналл и Мартин Хофманн (2005). «Зависимые типы». В Пирсе, Бенджамин К. (ред.) Расширенные темы по типам и языкам программирования . МТИ Пресс.

Внешние ссылки

• Официальный сайт , Хунвэй Си, дизайнер ATS, сопровождающий
• Домашняя страница DML. Архивировано 13 декабря 2009 г. на Wayback Machine.