Зависимый ML - Dependent ML

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

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

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

Рекомендации

  1. ^ Аспиналл и Хофманн 2005. стр. 75.

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

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

внешняя ссылка