Зависимый ML

This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these messages) This article provides insufficient context for those unfamiliar with the subject. Please help improve the article by providing more context for the reader. (March 2018) (Learn how and when to remove this message) The topic of this article may not meet Wikipedia's general notability guideline. Please help to demonstrate the notability of the topic by citing reliable secondary sources that are independent of the topic and provide significant coverage of it beyond a mere trivial mention. If notability cannot be shown, the article is likely to be merged, redirected, or deleted. Find sources: "Dependent ML" – news · newspapers · books · scholar · JSTOR (March 2018) (Learn how and when to remove this message) (Learn how and when to remove this message)

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

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

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

• Си, Хунвэй (март 2007 г.). «Зависимый ML: подход к практическому программированию с зависимыми типами». Журнал функционального программирования . 17 (2): 215–286. doi : 10.1017/S0956796806006216 . S2CID  45996427.
• Дэвид Аспиналл и Мартин Хофманн  [de] (2005). «Зависимые типы». В Pierce, Benjamin C. (ред.) Advanced Topics in Types and Programming Languages . MIT Press.

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

Эта статья, связанная с языком программирования, является заглушкой . Вы можете помочь Википедии, расширив ее.

• v
• t
• e