Стандартный ML


Standard ML ( SML ) — модульный функциональный язык программирования общего назначения с проверкой типов и выводом типов во время компиляции . Он популярен среди авторов компиляторов и исследователей языков программирования , а также среди разработчиков средств доказательства теорем .

Стандартный ML — это современный диалект ML , языка, используемого в проекте доказательства теорем «Логика для вычислимых функций » (LCF). Среди широко используемых языков он отличается тем, что имеет формальную спецификацию, представленную в виде правил типизации и операционной семантики в «Определении стандартного машинного обучения» . [4]

Стандартный ML — это функциональный язык программирования с некоторыми нечистыми функциями. Программы, написанные на стандартном ML, состоят из выражений , а не операторов или команд, хотя некоторые выражения типа unit оцениваются только на предмет их побочных эффектов .

Как и во всех функциональных языках, ключевой особенностью Standard ML является функция , которая используется для абстракции. Факториал можно выразить следующим образом:

Компилятор SML должен определить статический тип без предоставленных пользователем аннотаций типа. Он должен сделать вывод, что используется только с целочисленными выражениями и, следовательно, сам должен быть целым числом, и что все терминальные выражения являются целочисленными выражениями.val factorial : int -> intn

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