Стандартный ML - Standard ML
Парадигма | Мультипарадигма : функциональная , императивная , модульная |
---|---|
Семья | ML |
Впервые появился | 1983 |
Стабильный выпуск | Стандарт ML '97 / 1997
|
Печатная дисциплина | Предполагаемый , статический , сильный |
Расширения имени файла | .sml |
Веб-сайт | sml-family |
Основные реализации | |
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 -> int
n
Декларативные определения
Та же самая функция может быть выражена с помощью определений клаузальной функции, где условное выражение 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 Zero
p
h
_
Следует отметить, что такую же оптимизацию можно получить с помощью хвостового вызова .
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 queue
exception 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 TwoListQueue
signature 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 ::
[]
cmp
cmp
Расколоть
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 part
op <<
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 -> b
a * c -> b
a
c
c -> (a * c -> b) -> a -> b
В этом примере вычисляется числовая производная заданной функции в точке :
fun d
f
x
- 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 -> real
d
delta
delta
- 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 : реализация, очень близкая к определению, интегрирующая сборщик мусора (который можно отключить) и управление памятью на основе регионов с автоматическим выводом регионов, нацеленная на поддержку приложений в реальном времени.
Производная
- Алиса : интерпретатор для Standard ML от Саарландского университета с поддержкой параллельного программирования с использованием фьючерсов , ленивых вычислений , распределенных вычислений через удаленные вызовы процедур и программирования ограничений.
- SML # : расширение SML, обеспечивающее полиморфизм записей и взаимодействие с языком C. Это обычный собственный компилятор, и его название не является намеком на работу на платформе .NET.
- SOSML : реализация, написанная на TypeScript , поддерживающая большую часть языка SML и отдельные части базовой библиотеки.
Исследовать
- 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 .
Смотрите также
использованная литература
- ^ a b «Программирование в стандартном машинном обучении: иерархии и параметризация» . Проверено 22 февраля 2020 .
- ^ a b c "SML '97" . www.smlnj.org .
- ^ a b "itertools - Функции, создающие итераторы для эффективного цикла - Документация Python 3.7.1rc1" . docs.python.org .
- ^ а б Робин Милнер; Мадс Тофте; Роберт Харпер; Дэвид Маккуин (1997). Определение стандартного машинного обучения (пересмотренное) . MIT Press. ISBN 0-262-63181-4.
- ^ а б Крис Окасаки (2000). «Нумерация в ширину: уроки из небольшого упражнения в разработке алгоритмов». Международная конференция по функциональному программированию 2000 . ACM.
- ^ a b Мэдс Тофте. «Стандартный язык ML» . Scholarpedia . Проверено 8 января 2020 .
- ^ a b Джейд Алглав; Энтони Си Джей Фокс; Самин Иштиак; Магнус О. Майрин; Сусмит Саркар; Питер Сьюэлл; Франческо Заппа Нарделли. Семантика Power и ARM многопроцессорный машинный код (PDF) . DAMP 2009. С. 13–24.
внешние ссылки
О стандартном ML
- Пересмотренное определение
- Стандартный проект семейства ML на GitHub
- Что такое SML?
- Что такое SML '97?
О преемнике ML
- преемник ML (sML) : эволюция ML с использованием Standard ML в качестве отправной точки
- HaMLet на GitHub : эталонная реализация для преемника ML
Практичный
Академический