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

Стандартный ML
Парадигма Мультипарадигма : функциональная , императивная , модульная
Семья ML
Впервые появился 1983 ; 38 лет назад ( 1983 )
Стабильный выпуск
Стандарт ML '97 / 1997 ; 24 года назад ( 1997 )
Печатная дисциплина Предполагаемый , статический , сильный
Расширения имени файла .sml
Веб-сайт sml-family .org
Основные реализации
SML / NJ , MLton
Диалекты
Алиса , Параллельное машинное обучение , Зависимое машинное обучение
Под влиянием
ML , Надежда , Паскаль
Под влиянием
Вяз , F # , F * , Haskell , OCaml , Python , Rust , Scala

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

Стандартный ML - это современный диалект ML , языка, используемого в проекте доказательства теорем Logic for Computable Functions (LCF). Он отличается от широко используемых языков тем, что имеет формальную спецификацию, представленную в виде правил типизации и операционной семантики в The Definition of Standard ML .

Язык

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

Функции

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

fun factorial n = 
    if n = 0 then 1 else n * factorial (n - 1)

Вывод типа

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

Декларативные определения

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

fun factorial 0 = 1
  | factorial n = n * factorial (n - 1)

Императивные определения

или итеративно:

fun factorial n = let val i = ref n and acc = ref 1 in
    while !i > 0 do (acc := !acc * !i; i := !i - 1); !acc
end

Лямбда-функции

или как лямбда-функция:

val rec factorial = fn 0 => 1 | n => n * factorial (n - 1)

Здесь ключевое слово valвводит привязку идентификатора к значению, fnвводит анонимную функцию и recпозволяет определению быть самодостаточным.

Местные определения

Инкапсуляция сохраняющего инвариант хвостово-рекурсивного жесткого цикла с одним или несколькими параметрами аккумулятора во внешней функции без инвариантов, как показано здесь, является распространенной идиомой в стандартном ML.

Используя локальную функцию, его можно переписать в более эффективном стиле хвостовой рекурсии:

local
    fun loop (0, acc) = acc
      | loop (m, acc) = loop (m - 1, m * acc)
in
    fun factorial n = loop (n, 1)
end

Синонимы типа

Синоним типа определяется ключевым словом type. Вот синоним типа для точек на плоскости и функций, вычисляющих расстояния между двумя точками и площадь треугольника с заданными углами по формуле Герона . (Эти определения будут использоваться в последующих примерах).

type loc = real * real

fun square (x : real) = x * x

fun dist (x, y) (x', y') =
    Math.sqrt (square (x' - x) + square (y' - y))

fun heron (a, b, c) = let
    val x = dist a b
    val y = dist b c
    val z = dist a c
    val s = (x + y + z) / 2.0
    in
        Math.sqrt (s * (s - x) * (s - y) * (s - z))
    end

Алгебраические типы данных

Стандартный ML обеспечивает сильную поддержку алгебраических типов данных (ADT). Тип данных можно рассматривать как непересекающееся объединение кортежей (или «сумму произведений»). Их легко определить и простой в использовании, в основном из - за сопоставления с образцом , а также большинство реализаций Standard ML шаблон-исчерпанность проверки и шаблон проверки избыточности.

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

Тип данных определяется ключевым словом datatype, например:

datatype shape
    = Circle   of loc * real      (* center and radius *)
    | Square   of loc * real      (* upper-left corner and side length; axis-aligned *)
    | Triangle of loc * loc * loc (* corners *)

Обратите внимание, что синоним типа не может быть рекурсивным; типы данных необходимы для определения рекурсивных конструкторов. (В данном примере это не проблема.)

Сопоставление с образцом

Шаблоны сопоставляются в том порядке, в котором они определены. Программисты на C могут использовать помеченные объединения , отправляя значения тегов, чтобы достичь того, что выполняет ML с типами данных и сопоставлением с образцом. Тем не менее, хотя программа C, снабженная соответствующими проверками, будет в некотором смысле столь же надежна, как соответствующая программа ML, эти проверки обязательно будут динамическими; Статические проверки ML обеспечивают надежные гарантии правильности программы во время компиляции.

Аргументы функции могут быть определены как шаблоны следующим образом:

fun area (Circle (_, r)) = Math.pi * square r
  | area (Square (_, s)) = square s
  | area (Triangle p) = heron p (* see above *)

Так называемая «клаузальная форма» определения функции, где аргументы определяются как шаблоны, является просто синтаксическим сахаром для выражения case:

fun area shape = case shape of
    Circle (_, r) => Math.pi * square r
  | Square (_, s) => square s
  | Triangle p => heron p

Проверка полноты

Проверка полноты шаблонов гарантирует, что каждому конструктору типа данных соответствует хотя бы один шаблон.

Следующий шаблон не является исчерпывающим:

fun center (Circle (c, _)) = c
  | center (Square ((x, y), s)) = (x + s / 2.0, y + s / 2.0)

В функции нет шаблона для Triangleслучая center. Компилятор выдаст предупреждение о том, что выражение case не является исчерпывающим, и если Triangleво время выполнения этой функции будет передано a , будет сгенерировано. exception Match

Проверка избыточности

Шаблон во втором предложении следующей (бессмысленной) функции является избыточным:

fun f (Circle ((x, y), r)) = x + y
  | f (Circle _) = 1.0
  | f _ = 0.0

Любое значение, которое будет соответствовать шаблону во втором предложении, также будет соответствовать шаблону в первом предложении, поэтому второе предложение недостижимо. Следовательно, это определение в целом демонстрирует избыточность и вызывает предупреждение во время компиляции.

Следующее определение функции является исчерпывающим и не является избыточным:

val hasCorners = fn (Circle _) => false | _ => true

Если элемент управления проходит за первым шаблоном ( Circle), мы знаем, что форма должна быть либо a, Squareлибо a Triangle. В любом из этих случаев мы знаем, что у формы есть углы, поэтому мы можем вернуться, trueне различая фактическую форму.

Функции высшего порядка

Функции могут использовать функции в качестве аргументов:

fun map f (x, y) = (f x, f y)

Функции могут создавать функции как возвращаемые значения:

fun constant k = (fn _ => k)

Функции также могут как потреблять, так и производить функции:

fun compose (f, g) = (fn x => f (g x))

Функция List.mapиз базовой библиотеки - одна из наиболее часто используемых функций высшего порядка в Standard ML:

fun map _ [] = []
  | map f (x :: xs) = f x :: map f xs

Более эффективная реализация с хвостовой рекурсией List.foldl:

fun map f = List.rev o List.foldl (fn (x, acc) => f x :: acc) []

Исключения

Исключения вызываются ключевым словом raiseи обрабатываются handleконструкцией сопоставления с образцом . Система исключений может реализовать нелокальный выход ; этот метод оптимизации подходит для следующих функций.

exception Zero;

fun prod xs = let
    fun p (0 :: _) = raise Zero
      | p (h :: t) = h * p t
      | p [] = 1
    in
        p xs handle Zero => 0
    end

Когда он поднят, элемент управления полностью покидает функцию . Рассмотрим альтернативу: значение 0 будет возвращено в самый последний ожидающий кадр, оно будет умножено на локальное значение , полученное значение (неизбежно 0) будет возвращено в следующий ожидающий кадр и так далее. Возникновение исключения позволяет обойти всю цепочку кадров и избежать связанных вычислений. Обратите внимание на использование символа подчеркивания ( ) как шаблона подстановки. exception Zeroph_

Следует отметить, что такую ​​же оптимизацию можно получить с помощью хвостового вызова .

local
    fun p a (0 :: _) = 0
      | p a (x :: xs) = p (a * x) xs
      | p a [] = a
in
    val prod = p 1
end

Модульная система

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

Подписи

Подпись является интерфейс , обычно мыслится как тип для структуры; он определяет имена всех сущностей, предоставляемых структурой, а также арность каждого компонента типа, тип каждого компонента значения и сигнатуру каждой подструктуры. Определения компонентов типа необязательны; Компоненты типа, определения которых скрыты, являются абстрактными типами .

Например, подпись для очереди может быть:

signature QUEUE = sig
    type 'a queue
    exception QueueError;
    val empty     : 'a queue
    val isEmpty   : 'a queue -> bool
    val singleton : 'a -> 'a queue
    val fromList  : 'a list -> 'a queue
    val insert    : 'a * 'a queue -> 'a queue
    val peek      : 'a queue -> 'a
    val remove    : 'a queue -> 'a * 'a queue
end

Эта подпись описывает модуль , который обеспечивает полиморфный тип , и ценности , которые определяют основные операции по очереди. 'a queueexception QueueError

Структуры

Структура представляет собой модуль; он состоит из набора типов, исключений, значений и структур (называемых подструктурами ), упакованных вместе в логическую единицу.

Структура очереди может быть реализована следующим образом:

structure TwoListQueue :> QUEUE = struct
    type 'a queue = 'a list * 'a list

    exception QueueError;

    val empty = ([], [])

    fun isEmpty ([], []) = true
      | isEmpty _ = false

    fun singleton a = ([], [a])

    fun fromList a = ([], a)

    fun insert (a, ([], [])) = singleton a
      | insert (a, (ins, outs)) = (a :: ins, outs)

    fun peek (_, []) = raise QueueError
      | peek (ins, outs) = List.hd outs

    fun remove (_, []) = raise QueueError
      | remove (ins, [a]) = (a, ([], List.rev ins))
      | remove (ins, a :: outs) = (a, (ins, outs))
end

Это определение заявляет, что реализует . Более того, непрозрачное приписывание, обозначенное посредством, указывает, что любые типы, которые не определены в сигнатуре (т.е. ), должны быть абстрактными, что означает, что определение очереди как пары списков не видно за пределами модуля. Структура реализует все определения в подписи. structure TwoListQueuesignature QUEUE:>type 'a queue

Доступ к типам и значениям в структуре можно получить с помощью "точечной записи":

val q : string TwoListQueue.queue = TwoListQueue.empty
val q' = TwoListQueue.insert (Real.toString Math.pi, q)

Функторы

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

Один популярный алгоритм поиска в деревьях в ширину использует очереди. Здесь мы представляем версию этого алгоритма, параметризованную по абстрактной структуре очереди:

(* after Okasaki, ICFP, 2000 *)
functor BFS (Q: QUEUE) = struct
  datatype 'a tree = E | T of 'a * 'a tree * 'a tree

  local
    fun bfsQ q = if Q.isEmpty q then [] else search (Q.remove q)
    and search (E, q) = bfsQ q
      | search (T (x, l, r), q) = x :: bfsQ (insert (insert q l) r)
    and insert q a = Q.insert (a, q)
  in
    fun bfs t = bfsQ (Q.singleton t)
  end
end

structure QueueBFS = BFS (TwoListQueue)

Обратите внимание, что внутри представление очереди не видно. Более конкретно, нет способа выбрать первый список в очереди из двух списков, если это действительно используется представление. Этот механизм абстракции данных делает поиск в ширину по-настоящему независимым от реализации очереди. Это вообще желательно; в этом случае структура очереди может безопасно поддерживать любые логические инварианты, от которых зависит ее правильность за пуленепробиваемой стеной абстракции. functor BFS

Примеры кода

Фрагменты кода SML легче всего изучать, вводя их в интерактивный верхний уровень .

Привет, мир

Далее следует привет, мир! программа:

hello.sml
print "Hello, world!\n"
трепать
$ mlton hello.sml
$ ./hello
Hello, world!

Алгоритмы

Вставка сортировки

Сортировку вставкой (по возрастанию) можно кратко выразить следующим образом: int list

fun insert (x, []) = [x] | insert (x, h :: t) = sort x (h, t)
and sort x (h, t) = if x < h then [x, h] @ t else h :: insert (x, t)
val insertionsort = List.foldl insert []

Сортировка слиянием

Здесь классический алгоритм сортировки слиянием реализован в трех функциях: разделение, слияние и сортировка слиянием. Также обратите внимание на отсутствие типов, за исключением синтаксиса и обозначения списков. Этот код будет сортировать списки любого типа, если определена последовательная функция упорядочивания . Используя вывод типа Хиндли-Милнера , можно вывести типы всех переменных, даже сложных типов, таких как тип функции . op ::[]cmpcmp

Расколоть

fun splitреализован с закрытием с отслеживанием состояния, которое чередуется между trueи false, игнорируя ввод:

fun alternator {} = let val state = ref true
    in fn a => !state before state := not (!state) end

(* Split a list into near-halves which will either be the same length,
 * or the first will have one more element than the other.
 * Runs in O(n) time, where n = |xs|.
 *)
fun split xs = List.partition (alternator {}) xs

Объединить

Для повышения эффективности слияние использует локальный цикл функций. Внутренний loopопределяется в терминах случаев: когда оба списка непусты ( ) и когда один список пуст ( ). x :: xs[]

Эта функция объединяет два отсортированных списка в один отсортированный список. Обратите внимание, как аккумулятор accстроится в обратном порядке, а затем переворачивается перед возвратом. Это распространенный метод, поскольку он представлен в виде связанного списка ; этот метод требует больше часов, но асимптотика не хуже. 'a list

(* Merge two ordered lists using the order cmp.
 * Pre: each list must already be ordered per cmp.
 * Runs in O(n) time, where n = |xs| + |ys|.
 *)
fun merge cmp (xs, []) = xs
  | merge cmp (xs, y :: ys) = let
    fun loop (a, acc) (xs, []) = List.revAppend (a :: acc, xs)
      | loop (a, acc) (xs, y :: ys) =
        if cmp (a, y)
        then loop (y, a :: acc) (ys, xs)
        else loop (a, y :: acc) (xs, ys)
    in
        loop (y, []) (ys, xs)
    end

Сортировка слиянием

Основная функция:

fun ap f (x, y) = (f x, f y)

(* Sort a list in according to the given ordering operation cmp.
 * Runs in O(n log n) time, where n = |xs|.
 *)
fun mergesort cmp [] = []
  | mergesort cmp [x] = [x]
  | mergesort cmp xs = (merge cmp o ap (mergesort cmp) o split) xs

Быстрая сортировка

Быструю сортировку можно выразить следующим образом. это закрытие, которое потребляет оператор заказа . fun partop <<

infix <<

fun quicksort (op <<) = let
    fun part p = List.partition (fn x => x << p)
    fun sort [] = []
      | sort (p :: xs) = join p (part p xs)
    and join p (l, r) = sort l @ p :: sort r
    in
        sort
    end

Интерпретатор выражений

Обратите внимание на относительную легкость, с которой язык небольших выражений может быть определен и обработан:

exception TyErr;

datatype ty = IntTy | BoolTy

fun unify (IntTy, IntTy) = IntTy
  | unify (BoolTy, BoolTy) = BoolTy
  | unify (_, _) = raise TyErr

datatype exp
    = True
    | False
    | Int of int
    | Not of exp
    | Add of exp * exp
    | If  of exp * exp * exp

fun infer True = BoolTy
  | infer False = BoolTy
  | infer (Int _) = IntTy
  | infer (Not e) = (assert e BoolTy; BoolTy)
  | infer (Add (a, b)) = (assert a IntTy; assert b IntTy; IntTy)
  | infer (If (e, t, f)) = (assert e BoolTy; unify (infer t, infer f))
and assert e t = unify (infer e, t)

fun eval True = True
  | eval False = False
  | eval (Int n) = Int n
  | eval (Not e) = if eval e = True then False else True
  | eval (Add (a, b)) = (case (eval a, eval b) of (Int x, Int y) => Int (x + y))
  | eval (If (e, t, f)) = eval (if eval e = True then t else f)

fun run e = (infer e; SOME (eval e)) handle TyErr => NONE

Пример использования хорошо типизированных и нетипизированных выражений:

val SOME (Int 3) = run (Add (Int 1, Int 2)) (* well-typed *)
val NONE = run (If (Not (Int 1), True, False)) (* ill-typed *)

Целые числа произвольной точности

IntInfМодуль обеспечивает произвольную точность целочисленной арифметики. Более того, целочисленные литералы могут использоваться как целые числа произвольной точности, при этом программисту ничего не нужно делать.

Следующая программа реализует факториальную функцию произвольной точности:

fact.sml
fun fact n : IntInf.int = if n = 0 then 1 else n * fact (n - 1);

fun printLine str = let in
    TextIO.output (TextIO.stdOut, str);
    TextIO.output (TextIO.stdOut, "\n")
end;

val () = printLine (IntInf.toString (fact 120));
трепать
$ mlton fact.sml
$ ./fact
6689502913449127057588118054090372586752746333138029810295671352301
6335572449629893668741652719849813081576378932140905525344085894081
21859898481114389650005964960521256960000000000000000000000000000

Частичное применение

Каррированные функции имеют очень много приложений, например, для устранения избыточного кода. Например, модулю могут потребоваться функции типа , но удобнее писать функции типа, в которых существует фиксированная связь между объектами типа и . Функция типа может исключить эту общность. Это пример шаблона адаптера . a -> ba * c -> bacc -> (a * c -> b) -> a -> b

В этом примере вычисляется числовая производная заданной функции в точке : fun dfx

- fun d delta f x = (f (x + delta) - f (x - delta)) / (2.0 * delta)
val d = fn : real -> (real -> real) -> real -> real

Тип указывает на то, что он отображает "float" на функцию с этим типом . Это позволяет нам частично применять аргументы, известные как каррирование . В этом случае функцию можно специализировать, частично применив ее с аргументом . Хорошим выбором при использовании этого алгоритма является кубический корень машинного эпсилона . fun d(real -> real) -> real -> realddeltadelta

- val d' = d 1E~8;
val d' = fn : (real -> real) -> real -> real

Обратите внимание, что предполагаемый тип указывает, что d'ожидает функцию с типом в качестве первого аргумента. Мы можем вычислить приближение к производной at . Правильный ответ . real -> real

- d' (fn x => x * x * x - x - 1.0) 3.0;
val it = 25.9999996644 : real

Библиотеки

Стандарт

Базовая библиотека стандартизирована и поставляется с большинством реализаций. Он предоставляет модули для деревьев, массивов и других структур данных, а также интерфейсы ввода / вывода и системы.

Третья сторона

Для численных вычислений существует модуль Matrix (но в настоящее время он не работает) https://www.cs.cmu.edu/afs/cs/project/pscico/pscico/src/matrix/README.html .

Для графики cairo-sml - это интерфейс с открытым исходным кодом для графической библиотеки Cairo . Для машинного обучения существует библиотека графических моделей.

Реализации

Реализации Standard ML включают следующее:

Стандарт

  • HaMLet : интерпретатор стандартного машинного обучения , призванный быть точной и доступной эталонной реализацией стандарта.
  • MLton ( mlton.org ): оптимизирующий компилятор всей программы, который строго соответствует определению и производит очень быстрый код по сравнению с другими реализациями ML, включая бэкэнды для LLVM и C
  • Moscow ML : облегченная реализация, основанная на среде исполнения CAML Light, которая реализует полный язык Standard ML, включая модули и большую часть базовой библиотеки.
  • Poly / ML : полная реализация Standard ML, которая создает быстрый код и поддерживает многоядерное оборудование (через потоки Posix); его система времени выполнения выполняет параллельную сборку мусора и онлайн-совместное использование неизменяемых подструктур.
  • Стандартный ML Нью-Джерси ( smlnj.org ): полный компилятор со связанными библиотеками, инструментами, интерактивной оболочкой и документацией с поддержкой Concurrent ML.
  • SML.NET : стандартный компилятор машинного обучения для среды CLR с расширениями для связывания с другим кодом .NET.
  • ML Kit : реализация, очень близкая к определению, интегрирующая сборщик мусора (который можно отключить) и управление памятью на основе регионов с автоматическим выводом регионов, нацеленная на поддержку приложений в реальном времени.

Производная

Исследовать

  • CakeML - это REPL-версия ML с официально проверенным временем выполнения и переводом на ассемблер.
  • Isabelle ( Isabelle / ML ) интегрирует параллельный Poly / ML в интерактивную программу доказательства теорем со сложной IDE (на основе jEdit ) для официального Standard ML (SML'97), диалектом Isabelle / ML и языком доказательства. Начиная с Isabelle2016, есть также отладчик исходного кода для ML.
  • Poplog реализует версию Standard ML вместе с Common Lisp и Prolog , что позволяет программировать на разных языках; все они реализованы в POP-11 , который компилируется постепенно .
  • TILT - это компилятор с полной сертификацией для Standard ML, который использует типизированные промежуточные языки для оптимизации кода и обеспечения корректности, а также может компилироваться на типизированный язык ассемблера .

Все эти реализации имеют открытый исходный код и находятся в свободном доступе. Большинство из них реализованы в Standard ML. Коммерческих реализаций больше нет; Harlequin , ныне несуществующий, когда-то создал коммерческую среду IDE и компилятор под названием MLWorks, которые перешли в Xanalys и позже стали открытыми после того, как были приобретены Ravenbrook Limited 26 апреля 2013 года.

Основные проекты с использованием SML

IT Университет Копенгагена всего «s архитектуры предприятия реализуется примерно 100000 линий SML, в том числе отчетов о персонале, заработной платы, управление курса и обратной связи, управление проектами, студент и интерфейсов веб-самообслуживания.

В доказательство помощники HOL4 , Изабель , LEGO , и Twelf написаны в Standard ML. Он также используется разработчиками компиляторов и разработчиками интегральных схем, такими как ARM .

Смотрите также

использованная литература

  1. ^ a b «Программирование в стандартном машинном обучении: иерархии и параметризация» . Проверено 22 февраля 2020 .
  2. ^ a b c "SML '97" . www.smlnj.org .
  3. ^ a b "itertools - Функции, создающие итераторы для эффективного цикла - Документация Python 3.7.1rc1" . docs.python.org .
  4. ^ а б Робин Милнер; Мадс Тофте; Роберт Харпер; Дэвид Маккуин (1997). Определение стандартного машинного обучения (пересмотренное) . MIT Press. ISBN 0-262-63181-4.
  5. ^ а б Крис Окасаки (2000). «Нумерация в ширину: уроки из небольшого упражнения в разработке алгоритмов». Международная конференция по функциональному программированию 2000 . ACM.
  6. ^ a b Мэдс Тофте. «Стандартный язык ML» . Scholarpedia . Проверено 8 января 2020 .
  7. ^ a b Джейд Алглав; Энтони Си Джей Фокс; Самин Иштиак; Магнус О. Майрин; Сусмит Саркар; Питер Сьюэлл; Франческо Заппа Нарделли. Семантика Power и ARM многопроцессорный машинный код (PDF) . DAMP 2009. С. 13–24.

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

О стандартном ML

О преемнике ML

  • преемник ML (sML) : эволюция ML с использованием Standard ML в качестве отправной точки
  • HaMLet на GitHub : эталонная реализация для преемника ML

Практичный

Академический