Standard ML — Википедия
Standard ML | |
---|---|
Семантика | Формальная, ориентированная на интерпретацию |
Класс языка | аппликативный, функциональный, императивный |
Тип исполнения | общего назначения |
Появился в | 1984[1], 1990[2], 1997[3] |
Автор | Робин Милнер и другие |
Расширение файлов | .sml |
Выпуск | Standard ML '97 (1997 ) |
Система типов | Хиндли — Милнера |
Основные реализации | много |
Диалекты | Alice , SML# , Manticore и другие |
Испытал влияние | Lisp, ISWIM, ML, POP-2[англ.], Hope, Clear[англ.][4] |
Повлиял на | Erlang, OCaml, Haskell, successor ML (sML) |
Лицензия | открытое ПО |
Сайт | sml-family.org |
Платформа | x86, AMD64, PowerPC, ARM, SPARC, S390, DEC Alpha, MIPS, HPPA, PDP-11, JVM, .Net, LLVM, C--, TAL[англ.], Си[5], Ada[6] |
ОС | *BSD, Linux (Debian, Fedora и др.), Windows, Cygwin, MinGW, Darwin, Solaris, Hurd, AIX, HP-UX |
Standard ML (SML) — компилируемый язык программирования общего назначения высшего порядка[англ.], основанный на системе типов Хиндли — Милнера.
Является «в основном функциональным» языком[7][8], то есть поддерживает большинство технических свойств функциональных языков, но также предоставляет развитые возможности императивного программирования при необходимости. Сочетает устойчивость программ, гибкость на уровне динамически типизируемых языков и быстродействие на уровне языка Си; обеспечивает превосходную поддержку как быстрого прототипирования, так и модульности и крупномасштабного программирования[англ.][9][10].
SML был первым самостоятельным компилируемым языком в семействе ML и до сих пор служит опорным языком в сообществе по развитию ML (successor ML)[11]. В SML впервые была реализована уникальная аппликативная система модулей — язык модулей ML.
Общие сведения
[править | править код]Язык изначально ориентирован на крупномасштабное программирование[англ.] программных систем: он предоставляет эффективные средства абстракции и модульности, обеспечивая высокий коэффициент повторного использования кода, и это делает его подходящим также для быстрого прототипирования программ, в том числе и крупномасштабных[англ.]. Например, в процессе разработки (тогда ещё экспериментального) компилятора SML/NJ[англ.] (60 тысяч строк на SML), порой приходилось вносить радикальные изменения в реализации ключевых структур данных, влияющих на десятки модулей — и новая версия компилятора была готова в течение дня.[9] (см. также ICFP Programming Contest за 2008, 2009.) При этом, в отличие многих других языков, подходящих для быстрого прототипирования, SML может очень эффективно компилироваться .
SML известен своим относительно низким порогом вхождения и служит языком обучения программированию во многих университетах мира[12]. Обширно документирован в рабочем виде, активно используется учёными в качестве базы для исследования новых элементов языков программирования и идиом (см., например, полиморфизм структурных типов). К настоящему времени все реализации языка (включая устаревшие) стали открытыми и свободными.
Отличительные особенности
[править | править код]Язык имеет математически точное (англ. rigorous) формальное определение, называемое «Определением» (англ. The Definition). Для Определения построено доказательство полной типобезопасности, что гарантирует устойчивость программ и предсказуемое поведение даже при некорректных входных данных и возможных ошибках программистов. Даже содержащая ошибку программа на SML всегда продолжает вести себя как ML-программа: она может навечно уйти в расчёты или породить исключение, но она не может обрушиться[13].
SML является в основном функциональным (mostly functional или primarily functional) языком[7][8], то есть поддерживает большинство технических свойств функциональных языков, но также предоставляет возможности императивного программирования. Его чаще называют «языком высшего порядка[англ.]», чтобы подчеркнуть поддержку первоклассных функций и при этом отличить его от ссылочно-прозрачных языков.
SML реализует выдающиеся средства поддержки крупномасштабного программирования[англ.] за счёт наиболее мощной и выразительной системы модулей среди известных (язык модулей ML). В SML реализована ранняя версия языка модулей, являющаяся отдельным слоем языка: модули могут содержать объекты ядра языка, но не наоборот[14].
В отличие многих других языков семейства ML (OCaml, Haskell, F#, Felix, Opa, Nemerle и других), SML весьма минималистичен: он не имеет изначально встроенных средств объектно-ориентированного программирования, средств конкурентности, ad-hoc-полиморфизма, динамической типизации, генераторов списков и многих других возможностей. Однако, SML отличается ортогональностью[15] (то есть реализует минимально необходимый, но полный набор максимально различных элементов), что позволяет сравнительно легко эмулировать прочие возможности, и необходимые для этого приёмы широко освещены в литературе . Фактически, SML позволяет использовать сколь угодно высокоуровневую функциональность в качестве примитивной для реализации функциональности ещё более высокого уровня[16]. В частности, построены модели реализации классов типов и монад с использованием только стандартных конструкций SML, а также средств объектно-ориентированного программирования[17]. Более того, SML является одним из немногих языков, в котором непосредственно реализованы продолжения первого класса.
Возможности
[править | править код]- Мощная выразительная система типов
Система типов Хиндли — Милнера (Х-М) является отличительной особенностью ML и его потомков. Она обеспечивает надёжность программ за счёт раннего выявления ошибок, высокий коэффициент повторного использования кода, высокий потенциал к оптимизации, сочетая эти качества с немногословностью и выразительностью на уровне динамически типизируемых языков. Наиболее характерными чертами, присущими Х-М, являются полиморфизм типов, а также алгебраические типы данных и сопоставление с образцом на них.
Реализация Х-М в SML имеет следующие особенности:
- поддерживается полная абстракция и единообразие типов: любой конструктор типов применим к любому типу, и вводимые пользователем типы используются неотличимо от встроенных[18]
- полиморфизм типов ограничен пренексным полиморфизмом и имеет дополнительные ограничения
- отдельное место отводится типам, допускающим проверку на равенство (equality types)
- выведение почти всех типов (за единичными исключениями)
- Разнообразие встроенных разновидностей типов-произведений, используемых без необходимости предварительного объявления:
- исключения имеют особую семантику: тип исключения является единственным в языке расширяемым типом (extensible type), то есть всякое определение
exception X
вводит в программу новую конструирующую функциюX
для типаexn
. Как следствие, определения исключений являются порождающими, то есть повторение идентичного определенияexception Foo exception Foo
вводит два разных конструктора, несовместимых друг с другом, и из-за совпадения имён второй заслоняет видимость первого. Это делает механизм динамической обработки исключений статически типобезопасным (но не гарантирует отсутствие необработанных исключений — соответствующие доработки системы типов были предложены много позже — см. полиморфизм управляющих конструкций).
- Поддержка функционального программирования
- «всё — выражение» (англ. everything is an expression)
- все функции являются объектами первого класса (представленными в виде замыканий)
- доступно каррирование для функций (но не для конструкторов типов)
- по умолчанию все объявляемые значения константны
- лексическая область видимости (позволяющее инкапсулировать изменяемое состояние в функции)
- лямбда-абстракция
- гарантия оптимизации хвостовых вызовов (это особенно важно для эффективной реализации продолжений — см. программирование в стиле передачи продолжений)
- рекурсивные типы данных[англ.]
- Поддержка императивного программирования
- последовательное исполнение выражений в однозначном порядке (слева направо)[19]
- мутабельные ячейки, аккуратно обособленные в системе типов в виде ссылок, обеспечивающих полную безопасность по типам и по доступу к памяти (и за их счёт возможность эмуляции вызова по ссылке)
- мутабельные массивы (отдельно от константных, которые также доступны)
- обработка исключений
- цикл
while
- полное сохранение «духа ML» в императивных участках кода и возможность их безопасного смешивания с чистыми[20].
- Обеспечение высокой эффективности программ
- энергичная семантика передачи параметров
- мутабельные ячейки
- стандартная поддержка нескольких разновидностей массивов: константных (
Vector
) и мутабельных (Array
), в том числе двухмерных (Array2
), мономорфных (MonoVector
,MonoArray
) и полиморфных; а также их некопирующих срезов. Строковые типы, как и в Си, реализованы посредством массивов символов (то есть типstring
определён какchar vector
), и также доступны их некопирующие срезы (типsubstring
). - гарантия оптимизации хвостовых вызовов
- полное статическое разрешение типов всех выражений, включая полиморфную проверку значений на равенство, с полным удалением информации о типах в целевом коде (но остаётся контроль переполнения)
- (в некоторых реализациях) очень тонкий и быстрый FFIкаламбуров типизации, ручной контроль над сборщиком мусора и другие нестандартные особенности , доступность
Способы использования
[править | править код]В отличие от многих языков, SML предоставляет большое многообразие способов своего использования[21]:
- интерактивное доказательство теорем
- REPL и явная загрузка модулей
- инкрементальная компиляция[англ.] (традиционная для потомков Лиспа)
- пакетная компиляция (традиционная для потомков Алгола и BCPL)
- полнопрограммно-оптимизирующая компиляция (порой позволяющая конкурировать в быстродействии с Си — см. MLton )
- интерпретация (очень редко)
При этом в определённых режимах возможны самые разные целевые платформы и стратегии компиляции
:- в машинный код (на данный момент покрывается порядка десятка семейств архитектур; теоретически кроссплатформенность может быть существенно шире, чем у всех потомков Алгола и BCPL, за счёт более высокого уровня абстракции от машинного языка[22], и в каждом случае потенциально возможно создание эффективно оптимизирующего компилятора)
- в общепринятые байт-коды (JVM, .Net)
- в собственные байт-коды
- в языки программирования общего назначения семантически более низкого уровня (Си, Ada, Java, Ассемблер — только пакетно или полнопрограммно)
- в другие диалекты ML (см. Isabelle (система автоматического доказательства теорем) и преобразование программ[англ.])
Сами стратегии компиляции также существенно различаются:
- преобразование замыканий[англ.], в стиле передачи продолжений, представление адресов функций глобальным вариантным типом.
- сохранение явных потоков исходного кода, автоматическое распараллеливание, уплощение многопоточного исходного кода до линейного.
- обёрнутое (boxed) или не-обёрнутое (unboxed) представление примитивных типов
- динамическая или статическая сборка мусора, в одном потоке с приложением или в отдельном, полностью автоматическая или с возможностью явного контроля.
Язык
[править | править код]Базовая семантика
[править | править код]Этот раздел не завершён. |
Объявления, выражения, блоки, функции
[править | править код]Примитивные типы
[править | править код]Составные и определяемые типы
[править | править код]Мутабельные значения
[править | править код]Ограничение на значения
[править | править код]Ограничение на значения (англ. value restriction)
Управляющие конструкции
[править | править код]Крупномасштабное программирование
[править | править код]
Модульность
[править | править код]
Система модулей SML является наиболее развитой системой модулей в языках программирования. Она повторяет семантику ядра ML (англ. Core ML), так что зависимости между крупными компонентами программ строятся подобно зависимостям мелкого уровня. Эта система модулей состоит из трёх видов модулей:
- структур (
structure
) - сигнатур (
signature
) - функторов (
functor
)
Структуры похожи на модули в большинстве языков программирования. Сигнатуры служат интерфейсами структур, но не привязываются жёстко к определённым структурам, а выстраивают отношения по схеме «многие-ко-многим», позволяя гибко управлять видимостью компонентов структур в зависимости от нужд контекста программы.
Функторы представляют собой «функции над структурами», позволяя разрывать зависимости времени компиляции и описывать параметризованные модули. Они дают возможность типобезопасным образом описывать вычисления над компонентами программ, которые в других языках могут реализовываться только посредством метапрограммирования[23] — как шаблоны C++, только без боли и страданий[24], или макроязык Лиспа, только со статическим контролем безопасности порождаемого кода[23]. Большинство языков вовсе не имеют ничего, сравнимого с функторами[25].
Принципиальным отличием языка модулей ML является то, что результат функтора может включать не только значения, но и типы, причём они могут зависеть от типов, входящих в состав параметра функтора. Этим модули ML оказываются наиболее близки в своей выразительности к системам с зависимыми типами, но, в отличие от последних, модули ML могут быть редуцированы в плоскую Систему Fω[англ.] (см. Язык модулей ML#F-преобразование Россберга — Руссо — Дрейера).
Синтаксис и синтаксический сахар
[править | править код]Синтаксис языка очень краток, по количеству зарезервированных слов занимает промежуточную позицию между Haskell и Pascal[26].
SML имеет контекстно-свободную грамматику, хотя в ней отмечены некоторые неоднозначности. SML/NJ[англ.] использует LALR(1), но в одном месте присутствует LALR(2).
Список ключевых слов языка (совпадающие с ними идентификаторы не допускаются)[27]:
abstype and andalso as case datatype do else end eqtype exception fn fun functor handle if in include infix infixr let local nonfix of op open orelse raise rec sharing sig signature struct structure then type val where while with withtype
Допустимы также символьные идентификаторы — то есть имена типов, данных и функций могут состоять из следующих небуквенных символов:
! % & $ # + - * / : < = > ? @ \ ~ ' ^ |
Имена из этих символов могут быть любой длины[27]:
val ----> = 5 fun !!?©**??!! x = x - 1 infix 5 $^$^$^$ fun a $^$^$^$ b = a + b val :-|==>-># = List.foldr
Разумеется, использование таких имён на практике не желательно, но если предыдущий автор поддерживаемого кода их интенсивно применял, то благодаря формальному определению, становится возможным (и SML сам позволяет довольно легко эту задачу решить) написание препроцессора для исправления мнемоники.
Исключаются лишь следующие цепочки символов:
: | = => -> # :>
Причина этого ограничения заключена в их особой роли в синтаксисе языка:
:
— явное аннотирование типа значения|
— разделение образцов=
— отделение тела функции от её заголовка=>
— отделение тела лямбда-функции от её заголовка->
— конструктор функционального (стрелочного) типа#
— доступ к полю записи:>
— сопоставление структуры с сигнатурой
В SML не предусмотрено встроенного синтаксиса для массивов и векторов (константных массивов). Некоторые реализации в той или иной мере поддерживают синтаксис для массивов ([|1,2,3|]
) и векторов (#[1,2,3]
) в качестве расширения.
Операция присваивания записывается как в языках семейства Паскаль: x:=5
Экосистема языка
[править | править код]Стандартная библиотека
[править | править код]Стандартная библиотека SML носит название Базиса (англ. Basis). Она формировалась много лет, пройдя тщательное тестирование на реальных задачах на базе SML/NJ[англ.] , её черновик был опубликован в 1996 году[28], и затем её спецификация была официально издана в 2004 году[29]. В этот период уже появлялись руководства по её использованию[30]. Базисная библиотека реализует лишь необходимый минимум модулей: тривиальные типы данных, арифметика над ними, ввод-вывод, платформенно-независимый интерфейс к операционной системе, и т. п., но не реализует более сложную функциональность (например, многопоточность). Многие компиляторы дополнительно представляют различные экспериментальные библиотеки.
Компиляторы могут использовать знания о Базисе для применения заранее оптимизированных алгоритмов и специализированных техник оптимизации: например, MLton использует нативное представление типов Базиса (в точности соответствующее примитивным типам языка Си), а также простейших агрегатных типов, составленных из них.
Как и в большинстве языков, в Базисе SML действует ряд определённых архитектурных и синтаксических соглашений. Прежде всего это тривиальные составляющие стандартных структур, таких как сходные по названию и сигнатурам комбинаторы (такие как fold
). Далее, это распространяющаяся на большинство типов схема преобразования в строковый тип и обратно .
Конверторы и сканеры
[править | править код]Стандартная схема преобразования в строковый тип и обратно инкапсулирована в структуру StringCvt
:
structure StringCvt : sig datatype radix = BIN | OCT | DEC | HEX datatype realfmt = SCI of int option | FIX of int option | GEN of int option | EXACT type ('a, 'b) reader = 'b -> ('a * 'b) option val padLeft : char -> int -> string -> string val padRight : char -> int -> string -> string val splitl : (char -> bool) -> (char, 'a) reader -> 'a -> (string * 'a) val takel : (char -> bool) -> (char, 'a) reader -> 'a -> string val dropl : (char -> bool) -> (char, 'a) reader -> 'a -> 'a val skipWS : (char, 'a) reader -> 'a -> 'a type cs val scanString : ((char, cs) reader -> ('a, cs) reader) -> string -> 'a option end
Схема преобразования не ограничивается перечислением обоснований систем счисления, как в Си (BIN
, OCT
, DEC
, HEX
). Она распространяется на программирование высшего порядка[англ.], позволяя описывать операции чтения значений конкретных типов из абстрактных потоков и записи в них, и затем преобразовывать простые операции в более сложные посредством комбинаторов. В роли потоков могут выступать как стандартные потоки ввод-вывода, так и просто агрегатные типы, такие как списки или строки.[31]
Ключевым ингредиентом этой схемы являются ридеры, то есть значения типа ('a,'b) reader
. Интуитивно, ридер — это функция, которая принимает на вход поток типа 'b
и предпринимает попытку считать из него значение типа 'a
, возвращая либо считанное значение и «остаток» потока, либо NONE
в случае неудачи. Важной разновидностью ридеров являются сканеры, или сканирующие функции. Для данного типа T
сканирующая функция имеет тип
(char,'b) reader -> (T,'b) reader
— то есть представляет собой конвертор из ридера символов в ридер данного типа. Сканеры входят в состав многих стандартных модулей, например, сигнатура INTEGER
включает сканер для целых чисел:
signature INTEGER = sig eqtype int ... val scan : StringCvt.radix -> (char, 'a) StringCvt.reader -> 'a -> (int * 'a) option end
Числа считываются атомарным образом, но ридеры могут считывать из потоков и цепочки поэлементно, например, посимвольно строку из строки:
fun stringGetc (s) = let val ss = Substring.full (s) in case Substring.getc (ss) of NONE => NONE | SOME (c,ss') => SOME (c,Substring.string (ss')) end; stringGetc ("hello"); (* val it = SOME (#"h","ello") : (char * string) option *) stringGetc ( #2(valOf it) ); (* val it = SOME (#"e","llo") : (char * string) option *) stringGetc ( #2(valOf it) ); (* val it = SOME (#"l","lo") : (char * string) option *) stringGetc ( #2(valOf it) ); (* val it = SOME (#"l","o") : (char * string) option *) stringGetc ( #2(valOf it) ); (* val it = SOME (#"o","") : (char * string) option *) stringGetc ( #2(valOf it) ); (* val it = NONE : (char * string) option *)
Сканеры позволяют создавать ридеры из имеющихся ридеров, например:
val stringGetInt = Int.scan StringCvt.DEC stringGetc
Структура StringCvt
предоставляет также ряд вспомогательных функций. Например, splitl
, takel
и dropl
комбинируют символьные ридеры с символьными предикатами, позволяя фильтровать потоки.
Следует отметить, что не символьные ридеры являются особым случаем ридеров вообще, а наоборот[32]. Причина этого в том, что извлечение подпоследовательности из последовательности представляет собой обобщение извлечения подстроки из строки.
Портирование
[править | править код]Большинство реализаций языка достаточно строго соответствуют Определениюввода-вывода и т. д.). Однако, Определение предъявляет лишь минимальные требования к составу начального базиса, так что единственный обозримый результат корректной программы согласно Определению состоит в том, что программа завершается либо порождает исключение, и большинство реализаций совместимы на этом уровне[33].
. Различия заключаются в технических деталях, таких как бинарный формат раздельно компилируемых модулей, реализация FFI и др. На практике, реальная программа должна отталкиваться от некоего базиса (минимального набора типов, средствОднако, даже в стандартном Базисе[33], константа Int.maxInt
содержит значение наибольшего возможного целого, упакованное в опциональный тип[англ.], и его необходимо извлекать либо сопоставлением с образцом, либо вызовом функции valOf
. Для типов конечной размерности значение IntN.maxInt
равно SOME(m)
, и использование обоих способов извлечения равнозначно. Но IntInf.maxInt
равно NONE
, так что прямое обращение к содержимому через valOf
породит исключение Option
. По умолчанию IntInf
открыта, например, в компиляторе Poly/ML .
С определёнными усилиями возможна разработка программ, свободно портируемых между всеми актуальными реализациями языка. Примером такой программы является HaMLet
.Инструментарий разработки
[править | править код]
К настоящему времени Standard ML полностью стал достоянием общественности: все реализации являются бесплатными и открытыми и распространяются под самыми лояльными лицензиями (BSD-style, MIT); тексты Определения языка (как в версии 1990 года, так и в ревизированной версии 1997 года) и спецификации Базиса также доступны бесплатно .
SML имеет большое число реализаций. Значительная их часть написана на самом SML; исключение составляют рантаймы некоторых компиляторов, написанные на Си и Ассемблере, а также система Poplog[англ.] .
- SML/NJ (Standard ML of New Jersey) (основная статья[англ.])[34] — кроссплатформенный оптимизирующий компилятор. Поддерживает REPL и пакетную компиляцию. Является «канонической» реализацией SML, хотя и имеет множество отклонений от Определения[35]; служил инструментом разработки ряда других компиляторов и систем автоматического доказательства. Порождает нативный код для большого числа архитектур и ОС. FFI основан на динамической кодогенерации. Предоставляет ряд экспериментальных расширений, среди наиболее известных из которых можно отметить поддержку первоклассных продолжений, реализацию CML на их основе, одну из реализаций модулей высшего порядка (но не первого класса) и механизм квазицитирования[англ.] для встраивания языков[36][37]. Сопровождается богатой документацией.
- MLton (произносится «ми́лтон») (основная статья) (сайт проекта) — кроссплатформенный полнопрограммно-оптимизирующий компилятор. Обеспечивает для программ на SML быстродействие на уровне Си/C++ за счёт агрессивных оптимизаций, в том числе раскрытия рамок модулей, полной мономорфизации и дефункциализации[англ.] программы и нативного (необёрнутого и бестегового) представления примитивных типов, строк и массивов; имеет прямой FFI ; для длинной арифметики использует GnuMP. Порождает нативный код для большого числа архитектур под Unix-like ОС (под Windows требует Cygwin либо MinGW); имеет бэк-энды в Си, C--, LLVM. Включает полную Базисную библиотеку (даже все опциональные структуры), имеет свои порты множества характерных библиотек SML/NJ[англ.] , в том числе реализацию продолжений и CML . FFI обеспечивает вызовы в обоих направлениях (функций Си из кода на SML и наоборот), вплоть до взаимной рекурсии. Сопровождается очень богатой документацией, включая описание трюков с нетривиальным использованием языка, позволяющих расширять его полезными идиомами . Недостатками, вследствие глобального анализа и множества этапов преобразований, являются значительные затраты времени и памяти для работы.
- Poly/ML[38] — кроссплатформенный оптимизирующий компилятор. Порождает достаточно быстрый код, поддерживает многопроцессорные системы (на потоках POSIX), осуществляет параллельную сборку мусора, обеспечивая соиспользование неизменяемых структур данных; по умолчанию использует длинную арифметику (с сигнатурой
INTEGER
на верхнем уровне связана структураIntInf
). Предоставляет прямой интерфейс к WinAPI и X Window System. Бинарная реализация поставляется под Windows; под остальными ОС необходимо собирать исходные коды самостоятельно. Порождает нативный код для i386, PowerPC, SPARC, имеет бэк-энд в байт-код для работы на неподдерживаемых платформах. Poly/ML лежит в основе Isabelle (системы автоматического доказательства теорем), вместе с SML/NJ[англ.] . - ML Kit[39] — полнопрограммно-оптимизирующий компилятор. Ориентирован на разработку приложений реального времени: использует стратегию управления памятью на основе статического вывода регионов, позволяющую собирать мусор за константное время; а также нестандартную возможность временно выключать сборщик мусора вокруг критичных по скорости секций. Раскрывает рамки модулей — помимо повышения быстродействия это также важно для вывода регионов. Обеспечивает достаточно высокое быстродействие программ. Порождает нативный код для x86 под Windows и Unix, имеет также бэкенды в байт-код и в код на JavaScript. Из недостатков можно отметить отсутствие поддержки конкурентности и однонаправленность FFI (обеспечиваются вызовы из SML в Си, но не обратно).
- SML# (не путать с SML.NETнативный код и не имеет отношения к платформе .NET (SML# появился на несколько лет раньше). Порождает нативный код для x86 под POSIX. Начиная с версии 2.0, бэк-энд основан на LLVM, что позволит в дальнейшем расширить список поддерживаемых архитектур. В версии 3.0 была реализована поддержка x86-64 и полностью конкурентный сборщик мусора, обеспечивающий эффективное использование многоядерных систем и отсутствие пауз в работе программы. Обеспечивает неплохое быстродействие, в том числе за счёт нативного (необёрнутого и бестегового) представления примитивных типов и прямого FFI к Си и SQL; в ближайшем будущем планируются более сильные оптимизации. Включает также генератор красивой печати[англ.], генератор документации. ) — оптимизирующий компилятор SML с расширениями (формирующими диалект SML# ). Название не должно вводить в заблуждение, SML# компилирует в
- Manticore[40] — компилятор диалекта Manticore . Порождает нативный код для x86-64 под Linux и MacOS X. Работает в режиме REPL.
- CakeML[41] — компилятор с доказанной надёжностью. Реализует существенное подмножество Standard ML и написан сам на себе (включая рантайм). Как семантика языка, так и алгоритм компиляции описаны посредством логики высшего порядка и верифицированы, так что программы на CakeML преобразуются в семантически эквивалентный машинный код с доказанной надёжностью. Целью проекта является сделать системы интерактивного доказательства практичной платформой для прикладных разработок. На 2016 год порождает нативный код для x86-64, в ближайшем будущем планируется поддержка ещё ряда архитектур.
- TILT, или TIL-Two (исходные коды (Git)) — компилятор, основанный на идее использования в процессе компиляции исключительно типобезопасных промежуточных языков (Typed Intermediate Language, TIL — отсюда название), вплоть до типизированного ассемблера[англ.], с целью сохранения безопасности программы на всех этапах преобразований и оптимизации. Фронт-энд компилятора основан на семантике Харпера — Стоуна[42]. Разработан Робертом Харпером[англ.] с коллегами в исследовательских целях в середине 1990-х годов и с тех пор не поддерживается.
- FLINT (страница проекта на Yale.edu) аналогичен TILT , но внутренний язык не имеет выделенного исчисления модулей, при этом внешний язык поддерживает модули высшего порядка. FLINT был внедрён в состав SML/NJ, что повысило быстродействие последнего.[43]
- Alice — кроссплатформенный компилятор SML с расширениями (формирующими диалект Alice ) в байт-код виртуальной машины с поддержкой JIT. Ориентирован на разработку распределённых систем. Имеет собственную REPL-IDE со встроенным инспектором, которая позволяет компилировать выделяемые фрагменты кода (при условии их самодостаточности) и затем обеспечивает интерактивную информацию о выведенных типах. Поддерживается раздельная компиляция. Работает под Windows и различными Unix-like системами. В дополнение к стандартному Базису предоставляет ряд дополнительных библиотек, имеет интерфейс к SQLite и Gtk+. Сопровождается детальными руководствами по использованию предоставляемых языковых и библиотечных расширений (предполагающими знание SML).
- Moscow ML[44] — легковесный компилятор в байт-код. Основан на среде выполнения Caml Light, поддерживает REPL и пакетную компиляцию. Компилирует быстро, но оптимизация незначительна[45]. Предоставляет расширения языка (функторы высшего порядка, пакеты, квазицитирование[англ.]), имеет интерфейс к ряду системных и мультимедийных библиотек. Разработан в России в институте Келдыша под руководством Романенко А. С. для учебных целей; поддержку языка модулей с расширениями реализовал Клаудио Руссо (автор семантики пакетов).
- MLj — см. SML.NET
- SML.NET[46] — не путать с SML# — полнопрограммно-оптимизирующий компилятор для платформы .Net. Вырос из компилятора MLj для платформы JVM. Предоставляет интерфейс для связывания с другими .NET-языками. Имеет собственную систему анализа зависимостей между модулями. Компилирует только модули целиком, раскрывая их рамки. Управляется как из обычной командной строки, так из собственного режима REPL.
- SMLtoJs[47] — компилятор в исходный код на JavaScript. Осуществляет множественные оптимизации, в том числе раскрывает рамки модулей. Для работы использует MLton и ML Kit .
- sml2c[49] — компилятор в исходный код на Си. Сделан на основе внешнего интерфейса и среды выполнения SML/NJ[англ.] и поддерживает многие из его расширений (в том числе первоклассные продолжения). Порождает код на портируемом ANSI C, но из-за различий в свойствах семантики даёт 70-100% замедление по сравнению с прямой трансляцией SML в машинный код[5]. Работает только с определениями уровня модулей в пакетном режиме. Программы уровня модулей, компилируемые SML/NJ, могут компилироваться SML2c без изменений. В отличие от SML/NJ, не поддерживает отладку и профилирование на уровне исходного кода.
- RML-to-3GL — компилятор языка RML (подмножества языка четвёртого поколения SML) в исходный код на Ada (типобезопасного языка третьего поколения)[6]. По своему устройству похож на MLton[50]: использует мономорфизацию, дефункциализацию[англ.] и уплощение языка высшего порядка[англ.] до языка первого порядка.
- SML2Java — компилятор в исходный код на Java[51].
- HaMLet[52] — эталонная реализация SML. Представляет собой интерпретатор непосредственного, строка-к-строке, воплощения Определения языка. Не предназначен для промышленного применения — крайне неэффективен и предоставляет малоинформативные сообщения об ошибках — вместо этого он служит платформой для исследований самого языка и поиска возможных недостатков Определения. HaMLet сам полностью написан на SML (25 тыс.строк кода) без использования Си, и способность некоторого компилятора SML собрать коды HaMLet можно рассматривать как признак достаточно хорошей реализации Определения языка и Базисной библиотеки. В частности, коды HaMLet способны скомпилировать SML/NJ[англ.] , MLton , Moscow ML , Poly/ML , Alice , ML Kit , SML# , и, разумеется, он сам. HaMLet также имеет режим «HaMLet S», являющийся референсной реализацией текущей версии successor ML (sML). Разработан и поддерживается Андреасом Россбергом.
- Isabelle/ML[53] — компонент Isabelle (системы автоматического доказательства теорем) в стиле LCF[англ.] . Isabelle разработана под руководством Луки Карделли[англ.] на основе системы HOL-90. Включает в себя редактор, основанный на jEdit. Наиболее значимым компонентом Isabelle является Isabelle/HOL, который на основе исполнимых спецификаций позволяет порождать исходные коды на SML, OCaml, Haskell, Scala, а также документацию на основе вставок на LAΤΕΧ в исходном коде.
- Edinburgh LCF (Logic for Computable Functions) (основная статья[англ.]) (исходные коды доступны в составе Isabelle) — интерактивной системы доказательства теорем, исторически первая реализация корневого языка ML (до введения языка модулей и формирования SML).
- Poplog[англ.][54] — инкрементальный компилятор и интегрированная среда разработки, ориентированная на работу в сфере искусственного интеллекта. Предоставляет возможность смешивания одновременно нескольких языков, в число которых входит POP-11[англ.], Prolog, Common Lisp и SML. Внутреннее представление всех языков основано на POP-11[англ.] — Лиспо-подобном рефлективном языке; на нём же реализован сам Poplog. Включает в себя редактор, похожий на Emacs, и поддерживает GUI, но только под X Window System; под Windows предоставляет лишь консоль. Название Poplog представляет собой акроним из «POP-11» и «Prolog». Несмотря на то, что Poplog активно развивается, он отстал от развития языка SML: в настоящее время его реализация SML не соответствует актуальному Определению (SML'97) и не реализует Базисную библиотеку.
- MLWorks[55] — компилятор с полнофункциональной IDE и сопутствующим инструментарием. Ранее был коммерческим, разрабатывался компанией Harlequin[англ.] в 1990-е годы. На рубеже веков владелец сменился и поддержка была прекращена. В 2013 году обрёл нового владельца, который открыл исходные коды и организовал работу по реанимации проекта. По состоянию на 2016 год не работоспособен.
- Edinburgh ML (исходные коды) — компилятор ML, раскрученный на основе исторически первого компилятора ML, разработанного Лукой Карделли[англ.] Vax ML (второй реализации ML после Edinburgh LCF (Logic for Computable Functions)[англ.] ). Коды ныне открыты, но так как они не изменялись с 1980-х годов, в них по-прежнему указано, что язык ML не является общественным достоянием, и использование данного компилятора требует лицензирования.
- TILT — см. в разделе «верифицирующие компиляторы»
Диалекты, расширения
[править | править код]
SML#
[править | править код]SML#[56] консервативно расширяет SML полиморфизмом записей в модели Ацуси Охори, который в SML# используется для бесшовного встраивания SQL в код на SML для интенсивного database-программирования.
Символ решётки (#
) в названии языка символизирует селектор (операцию выбора поля из записи). Одноимённый компилятор претендует на хорошее быстродействие. Разработан и развивается в институте Тохоку (Япония) под руководством самого Охори.
Alice
[править | править код]Alice ML консервативно расширяет SML примитивами для конкурентного программирования на основе экзотичной стратегии вычисления «call by future (вызов по будущности)», решателем в ограничениях, а также всеми согласованными элементами проекта successor ML. В частности, Alice поддерживает модули первого класса в форме пакетов с динамической загрузкой и динамической типизацией, что позволяет реализовывать распределённые вычисления. Alice также наделяет будущности первоклассными свойствами, в том числе, предоставляя будущности уровня модулей (будущные структуры и будущные сигнатуры). Одноимённый компилятор использует виртуальную машину. Разработан и развивается в Саарландском университете под руководством Андреаса Россберга.
Concurrent ML
[править | править код]Concurrent ML (CML) — библиотека, воплощающая встраиваемый язык, который расширяет SML конструкциями конкурентного программирования высшего порядка[англ.] на основе модели синхронной передачи первоклассных сообщений. Входит в стандартную поставку компиляторов SML/NJ[англ.] и MLton. Ключевые идеи CML лежат в основе проекта Manticore и включены в проект successor ML[11].
Manticore
[править | править код]Manticore[40] реализует всестороннюю поддержку конкурентного и параллельного программирования, от логической декомпозиции системы на процессы до тонкого контроля за максимально эффективным использованием многоядерных систем. Manticore основан на подмножестве SML, исключая мутабельные массивы и ссылки, то есть является чистым языком, сохраняя строгий порядок вычисления. Механизмы явной конкурентности и грубого параллелизма (потоки) основаны на CML , а механизмы тонкого параллелизма уровня данных (параллельные массивы) — аналогичны NESL[англ.]. Одноимённый компилятор порождает нативный код.
MLPolyR
[править | править код]MLPolyR — игрушечный язык, основанный на простейшем подмножестве SML и дополняющий его несколькими уровнями типобезопасности. Целью проекта является глубокое исследование полиморфизма записей для нужд проекта successor ML. Инновационная система типов MLPolyR решает проблему выражения[англ.] и гарантирует отсутствие необработанных исключений в программах.
Разработан под руководством Матиаса Блюма (автора NLFFIТехнологическом Институте Тойота в Чикаго[англ.], США.
) вMythryl
[править | править код]Mythryl[57] — синтаксический вариант SML, нацеленный на повышение скорости разработки под POSIX. Новый синтаксис во многом заимствован из Си; терминология также пересмотрена под более традиционную (например, функторы переименованы в дженерики). При этом авторы подчёркивают, что не намерены создать «очередную свалку языковых возможностей», а придерживаются минималистичной природы SML и опираются на его Определение . Реализация является форком SML/NJ[англ.] .
Прочие
[править | править код]- MetaML и MacroML — расширение SML средствами порождающего программирования[58].
Утилиты
[править | править код]
- Compilation Manager (CM) и MLBasis System (MLB) — расширения компиляторов для лучшей поддержки модульности (контроля зависимостей). В принципе, для этой цели мог бы использоваться и традиционный для большинства языков make, но язык модулей SML значительно мощнее средств модульности других языков, а make его преимуществ не поддерживает, и не пригоден для работы в режиме REPL[59]. CM изначально реализован в SML/NJ[англ.], затем портирован на MLton. Позже в составе MLton была предложена система MLB и конвертор файлов формата .cm в формат .mlb. Поддержка MLB была добавлена в ML Kit.
- eXene[60] — библиотека графического интерфейса пользователя под X Window System. Реализует реактивную модель взаимодействия на основе CML . Поставляется с SML/NJ[англ.].
- MLLex, MLYacc, MLAntlr, MLLPT — генераторы лексеров и парсеров (см. Lex и Yacc).
Межъязыковое взаимодействие
[править | править код]
- Интерфейс внешних функций. В разных компиляторах имеет разную реализацию, что тесно связано с представлением данных (прежде всего, обёрнутое или необёрнутое, теговое или бестеговое). В SML/NJ FFI основан на динамической кодогенерации, и если функция принимает на вход данные общим объёмом
n
байт и возвращаетm
байт, то её вызов имеет сложностьn+m
[61]. Некоторые компиляторы (MLton , SML# ) используют необёрнутое и бестеговое представление данных и обеспечивают прямые обращения к функциям и данным Си. В последнем случае вынесение медлительных функций в код на Си может существенно повышать общее быстродействие программы[62]. - NLFFI (No-Longer-Foreign Function Interface — рус. интерфейс к отныне-более-не-чужеродным функциям)[63] — альтернативный, более высокоуровневый интерфейс внешних функций. NLFFI автоматически порождает связующий код, позволяя подключать
*.h
-файлы (заголовочные файлы Си) непосредственно в состав проекта на SML (CM или MLB ), что снимает необходимость ручного кодирования определений FFI . Конструктивно идея NLFFI состоит в моделировании системы типов Си посредством типов ML; реализация основана CKit . Поставляется с SML/NJ[англ.] и MLton. - CKit — фронт-энд языка Си, написанный на SML. Осуществляет трансляцию исходных кодов на Си (с учётом препроцессора) в AST, реализуемое посредством структур данных языка SML. Лежит в основе реализации NLFFI .
Идеоматика, соглашения
[править | править код]К оформлению программ на SML не предъявляется никаких требований, поскольку грамматика языка полностью контекстно-свободна и не содержит явных неоднозначностей. Тем не менее, в ней отмечаются частные проблемы, например, при передаче оператора умножения op *
закрывающую скобку необходимо отделять пробелом ((op * )
), так как при сплошном написании многие реализации (не все) принимают пару символов *)
за закрытие комментария в коде и выдают ошибку.
Однако, всё же существуют определённые рекомендации, нацеленные на улучшение читабельности, модульности и повторного использования кода, а также раннего обнаружения ошибок и повышения модифицируемости (но не для внесения информации о типах в идентификаторы, как это делается, например, в венгерской нотации)[64]. В частности, в SML рекомендуется правило именования идентификаторов уровня ядра языка, аналогичное тому, что требуется в Haskell: fooBar
для значений, foo_bar
для конструкторов типов, FooBar
для конструирующих функций (некоторые компиляторы даже выдают предупреждение при его нарушении). Это связано с особенностью работы механизма сопоставления с образцом, который в общем случае не способен отличить ввод локальной переменной от использования нуль-арного конструктора типов, так что опечатки могут приводить к (сравнительно легко обнаружимым) ошибкам[65].
Наиболее непривычными и неожиданными могут быть:
- предпочтение шага отступа в три символа (не в четыре)
- частое применение апострофа в идентификаторах (аналогично принятому в математике): если на основе
x
требуется построить «новый x», то в большинстве языков пишут «x1
», а в SML, как и в математике, зачастую «x'
» («икс-штрих»). - синтаксис бинарных логических операций «И» и «ИЛИ»:
andalso
иorelse
, соответственно.[66] - синтаксис инфиксных операций конкатенации строк и списков:
^
и@
, соответственно (для векторов и массивов не предусмотрены).
Процедуры
[править | править код]Для процедур принята та же идиома, что и в Си: процедуры представляются функциями, возвращающими значение единичного типа[англ.]:
fun p s = print s (* val p = fn : sting -> unit *)
Последовательные вычисления
[править | править код]Этот раздел не завершён. |
let D in E end
fun foo ... = let val _ = ... in ... end
Приёмы
[править | править код]Эта-расширение
[править | править код]Эта-расширение (англ. eta-expansion) выражения e
есть выражение fn z => e z
, то есть обёртка исходного выражения в лямбда-функцию, где z
не встречается в e
. Разумеется, это имеет смысл лишь в случае, если e
имеет стрелочный тип, то есть является функцией. Эта-расширение принуждает задержку вычисления e
до применения функции и повторное его вычисление при каждом применении. Этот приём применяется в SML для преодоления ограничений выразительности, связанных с семантикой ограничения на значения . Термин «эта-расширение» заимствован из эта-преобразования в лямбда исчислении, означающего, напротив, редукцию выражения fn z => e z
до e
в случае, если z
не встречается в e
(эта-сжатие).[67][68]
Значения, индексированные типами
[править | править код]Значения, индексированные типами (англ. type-indexed values) — это техника, позволяющая ввести в SML поддержку ad-hoc-полиморфизма (которая в нём изначально отсутствует)[69]. Существует целый ряд её вариантов, в том числе нацеленные на поддержку полноценного объектно-ориентированного программирования[17].
Fold
[править | править код]«Fold»[70] — это техника, позволяющая ввести в SML ряд распространённых идиом, включая функции с переменным числом аргументов, именованные параметры функций, значения параметров по умолчанию, синтаксическую поддержку массивов в коде, функциональное обновление записей и косметическое изображение зависимой типизации для обеспечения типобезопасности функций вроде printf
.
Необходимо определить три функции — fold
, step0
и $
— такие, чтобы было верно следующее равенство:
fold (a, f) (step0 h1) (step0 h2) ... (step0 hn) $ = f (hn (... (h2 (h1 a))))
Их минимальное определение немногословно:
fun $ (a, f) = f a structure Fold = struct fun fold (a, f) g = g (a, f) fun step0 h (a, f) = fold (h a, f) end
Более развитая реализация позволяет контролировать типы выражений с использованием Fold.
val sum = fn z => Fold.fold (0, fn s => s) z fun a i = Fold.step0 (fn s => i + s) ... sum (a 1) (a 2) (a 3) $ (* val it : int = 6 *)
val list = fn z => Fold.fold ([], rev) z val ‘ = fn z => Fold.step1 (op ::) z ... list ‘w ‘x ‘y ‘z $
val f = fn z => Fold.fold ((), id) z val a = fn z => Fold.step0 (fn () => "hello") z val b = fn z => Fold.step0 (fn () => 13) z val c = fn z => Fold.step0 (fn () => (1, 2)) z ... f a $ = "hello": string f b $ = 13: int f c $ = (1, 2): int * int
Примеры программ
[править | править код]
Hello World!
[править | править код]Простейшая программа на SML может быть записана в одну строку:
print "Hello World!\n"
Однако, учитывая ориентированность языка на крупномасштабное программирование[англ.], минимальной всё же следует считать её обёртку в язык модулей (некоторые компиляторы работают только с программами уровня модулей).
signature HELLO_WORLD = sig val helloworld : unit -> unit end structure HelloWorld : HELLO_WORLD = struct fun helloworld () = print "Hello World!\n" end
Точкой старта программы, вообще говоря, может быть выбрана любая функция, но на практике имеет смысл соблюдать общепринятые соглашения, поэтому стоит добавить такой код:
structure Main = struct fun main (name: string, args: string list) : OS.Process.status = let val _ = HelloWorld.helloworld () in OS.Process.success end end
Для компилятора SML/NJ[англ.] в структуру Main
требуется также дополнительно добавить специфичную строку:
val _ = SMLofNJ.exportFn ("project1", main);
Для многомодульных программ требуется также создать файл проекта для отслеживания зависимостей в менеджере компилятора (некоторые компиляторы делают это автоматически). Например, для SML/NJ следует создать файл с именем sources.cm
следующего содержания:
Group signature HELLO_WORLD structure HelloWorld is helloworld-sig.sml helloworld.sml end
Более универсальным с точки зрения поддержки различными компиляторами (но несколько более ограниченным по возможностям) вариантом может быть создание обычного файла исходного кода на SML с линейным перечислением подключаемых файлов:
use "helloworld-sig.sml"; use "helloworld.sml";
Выходной машинный код для минимальной программы также получается относительно крупным (в сравнении с реализаций Hello World на Си), поскольку даже самая маленькая программа на SML обязана включать в себя рантайм-систему языка, бо́льшую часть которой составляет сборщик мусора. Однако, не следует воспринимать размер исходного и машинного кодов на начальном этапе как тяжеловесность SML: их причиной является интенсивная ориентированность языка на разработку крупных и сложных систем. Дальнейшее наращивание программ происходит по существенно более пологой кривой, чем в большинстве других статически типизируемых языков, и оверхед становится едва заметным при разработке серьёзных программ[71].
Автоматическая вёрстка
[править | править код]fun firstLine s = let val (name, rest) = Substring.splitl (fn c => c <> #".") (Substring.full s) in "\n<P><EM>" ^ Substring.string name ^ "</EM>" ^ Substring.string rest end fun htmlCvt fileName = let val is = TextIO.openIn fileName and os = TextIO.openOut (fileName ^ ".html") fun cvt _ NONE = () | cvt _ (SOME "\n") = cvt true (TextIO.inputLine is) | cvt first (SOME s) = ( TextIO.output (os, if first then firstLine s else "<br>" ^ s); cvt false (TextIO.inputLine is) ) in cvt true (SOME "\n"); TextIO.closeIn is; TextIO.closeOut os end
Этот код преобразует по простейшим правилам плоский текст в HTML, оформляя диалог по ролям[72].
Допустим, есть следующий текстовый файл с именем Henry.txt
:
Westmoreland. Of fighting men they have full three score thousand. Exeter. There's five to one; besides, they all are fresh. Westmoreland. 0 that we now had here But one ten thousand of those men in England That do no work to-day! King Henry V. What's he that wishes so? My cousin Westmoreland? No, my fair cousin: If we are marked to die, we are enough To do our country loss; and if to live, The fewer men, the greater share of honour.
Тогда вызов программы следующей строкой:
val _ = htmlCvt "Henry.txt"
Создаст файл с именем Henry.txt.html
следующего содержания:
<P><EM>Westmoreland</EM>. Of fighting men they have full three score thousand. <P><EM>Exeter</EM>. There's five to one; besides, they all are fresh. <P><EM>Westmoreland</EM>. 0 that we now had here <br>But one ten thousand of those men in England <br>That do no work to-day! <P><EM>King Henry V</EM>. What's he that wishes so? <br>My cousin Westmoreland? No, my fair cousin: <br>If we are marked to die, we are enough <br>To do our country loss; and if to live, <br>The fewer men, the greater share of honour.
Этот файл можно открыть в браузере, увидев следующее:
Westmoreland. Of fighting men they have full three score thousand.
Exeter. There's five to one; besides, they all are fresh.
Westmoreland. 0 that we now had here
But one ten thousand of those men in England
That do no work to-day!King Henry V. What's he that wishes so?
My cousin Westmoreland? No, my fair cousin:
If we are marked to die, we are enough
To do our country loss; and if to live,
The fewer men, the greater share of honour.
Троичные деревья
[править | править код]Для задачи поиска строки в словаре троичные деревья[англ.] сочетают молниеносную скорость префиксных деревьев с экономичностью двоичных деревьев в отношении памяти.
type key = Key.ord_key type item = Key.ord_key list datatype set = LEAF | NODE of { key: key, lt: set, eq: set, gt: set } val empty = LEAF exception AlreadyPresent fun member (_, LEAF) = false | member (h::t, NODE {key,lt,eq,gt}) = (case Key.compare (h, key) of EQUAL => member(t, eq) | LESS => member(h::t, lt) | GREATER => member(h::t, gt) ) | member ([], NODE {key,lt,eq,gt}) = (case Key.compare (Key.sentinel, key) of EQUAL => true | LESS => member([], lt) | GREATER => member([], gt) ) fun insert(h::t, LEAF) = NODE { key=h, eq = insert(t, LEAF), lt=LEAF, gt=LEAF } | insert([], LEAF) = NODE { key=Key.sentinel, eq=LEAF, lt=LEAF, gt=LEAF } | insert(h::t, NODE {key,lt,eq,gt}) = (case Key.compare (h, key) of EQUAL => NODE {key=key, lt=lt, gt=gt, eq=insert(t, eq)} | LESS => NODE {key=key, lt=insert(h::t, lt), gt=gt, eq=eq} | GREATER => NODE {key=key, lt=lt, gt=insert(h::t, gt), eq=eq} ) | insert([], NODE {key,lt,eq,gt}) = (case Key.compare (Key.sentinel, key) of EQUAL => raise AlreadyPresent | LESS => NODE {key=key, lt=insert([], lt), gt=gt, eq=eq} | GREATER => NODE {key=key, lt=lt, gt=insert([], gt), eq=eq} ) fun add(l, n) = insert(l, n) handle AlreadyPresent => n
Этот код использует Базисную структуру Key
, сопоставимую с сигнатурой ORD_KEY
, а также глобальный тип order
(над которым, в частности, определена функция Key.compare
):
datatype order = LESS | EQUAL | GREATER
О языке
[править | править код]Быстродействие
[править | править код]Типичные преимущества функционального программирования (типобезопасность, автоматическое управление памятью, высокий уровень абстракции и др.) проявляются в обеспечении надёжности и вообще работоспособности программ, а в ответственных, особенно крупномасштабных[англ.] задачах быстродействие часто играет второстепенную роль. Упор на эти свойства исторически привёл к тому, что программистам на функциональных языках зачастую оказываются недоступны многие эффективные структуры данных (массивы, строки, битовые цепочки), поэтому функциональные программы обычно заметно менее эффективны, чем эквивалентные программы на Си.[73]
ML изначально предоставляет весьма неплохие средства для тонкого контроля за быстродействием , однако, исторически реализации ML были крайне медлительными. Тем не менее, ещё в начале 1990-х Эндрю Аппель[англ.] прочил[74] языку SML скорость исполнения выше скорости языка Си, по крайней мере при интенсивной работе со сложноструктурированными данными (но SML не претендует на то, чтобы быть заменой Си в задачах системного программирования). За следующие несколько лет напряжённая работа над развитием компиляторов привела к тому, что скорость исполнения программ на SML повысилась в 20-40 раз[75].
В конце 1990-х Стивен Уикс задался целью добиться от программ на SML максимально возможной производительности и написал дефункторизатор для SML/NJ[англ.] , сразу показавший прирост скорости ещё в 2-3 раза. Дальнейшая работа в этом направлении привела к созданию компилятора MLton , который к середине нулевых годов XXI века показывал прирост скорости перед другими компиляторами в среднем на два порядка[45], конкурируя с Си (подробнее см. MLton).
Стратегия автоматического управление памятью на основе вывода регионов позволяет устранять затраты на инициализацию и высвобождение памяти из исполнения программы (то есть реализует сборку мусора на этапе компиляции). Компилятор ML Kit использует эту стратегию, позволяя решать задачи реального времени, хотя он уступает MLton по возможностям оптимизации.
На основе фронт-енда SML/NJ[англ.] был разработан компилятор в исходный код на Си — sml2c . Он порождает код хорошего качества, но примечательно, что схема компиляции «сначала в Си, затем в машинный код» до двух раз снижает быстродействие по сравнению с прямой компиляцией SML в машинный код из-за семантических различий между SML и Си[5].
Некоторые компиляторы SML предоставляют возможность профилирования кода с целью определения функций, занимающих наибольшее процессорное время (причём результат всегда неожиданный)[73], после чего можно сосредоточиться на их оптимизации средствами SML, либо вынести их в код на Си через FFI .
Обоснование семантики
[править | править код]Общие сведения
[править | править код]Теоретической основой языка является полиморфно типизированное лямбда-исчисление (Система F), ограниченное Let-полиморфизмом.
«Определение» (The Definition)
[править | править код]Официальным «стандартом» языка является изданное в виде книги «Определение» (англ. The Definition). Определение сформулировано в строгих математических понятиях и имеет доказанную надёжность. Непротиворечивость Определения позволяет человеку без запуска конкретного компилятора проверить программу на корректность и вычислить её результат; но, с другой стороны, Определение требует высокой квалификации для понимания и не может служить учебником по языку[74].
Доказуемость надёжности не далась сама по себе — Определение было неоднократно пересмотрено прежде, чем увидело свет. Многие языки опираются на общие теории, но при разработке они почти никогда не проверяются на безопасность совместного использования конкретных языковых элементов, являющихся частными приложениями этих теорий, что неизбежно приводит к несовместимости между реализациями языка. Эти проблемы либо игнорируются, либо начинают преподноситься как естественное явление (англ. «not a bug, but a feature»), но в действительности их причиной является то, что язык не был подвергнут математическому анализу[76].
Первоначальное Определение, «The Definition of Standard ML», было издано в 1990 году[2]. Спустя год были изданы «Комментарии к Определению» («Commentary on Standard ML»), объясняющие применённые подходы и нотации[77]. Вместе они составляют спецификацию языка, ныне известного как «SML'90». В течение следующих лет появился ряд критических замечаний и предложений по улучшению (одним из наиболее известных среди которых являются просвечивающие суммы Харпера — Лилибриджа), и в 1997 году многие из них были собраны в ревизированной версии Определения, «The Definition of Standard ML: Revised»[3], определив версию языка «SML'97», сохраняющего обратную совместимость с прежним. Ревизированное Определение использует принципы, описанные в Комментариях 1991 года, так что намеревающимся досконально изучить Определение SML рекомендуется сначала изучать SML'90, и лишь затем SML'97.[78]
Со временем в тексте Определения был обнаружен ряд неоднозначностей и упущений[79][80][81]. Однако, они не умаляют строгости Определения по сути — доказательство его надёжности было механизировано в Twelf[англ.][82]. Большинство реализаций достаточно строго соответствуют Определению, отклоняясь в технических особенностях — бинарных форматах, FFI и пр., а также в особенностях трактовки неоднозначных мест в Определении — всё это приводит к необходимости приложения некоторых дополнительных усилий (существенно меньших, чем для большинства других языков) для обеспечения безупречной портируемости реальных программ на SML между реализациями (небольшие программы в большинстве случаев не имеют проблем портирования).
Определение SML является примером структурной операционной семантики[англ.]!!; оно является не первым формальным определением языка, но первым, однозначно понятным разработчикам компиляторов[83].
Определение оперирует семантическими объектами (semantic objects), описывая их смысл (meaning). Во введении авторы делают акцент на том, что именно семантические объекты (к числу коих, в зависимости от конкретного языка, могут относиться такие понятия как пакет, модуль, структура, исключение, канал, тип, процедура, ссылка, соиспользование и пр.), а не синтаксис, определяют концептуальное представление о языке программирования, и именно на них должно строиться определение всякого языка[84].
Согласно Определению, SML разделяется на три языка, надстроенные один над другим: нижний слой, называемый «Ядром языка» (Core language), средний слой, называемый «Модулями» (Modules) и небольшой верхний слой, называемый «Программами» (Programs), представляющий собой совокупность определений верхнего уровня (top-level declarations).
Определение включает около 200 правил вывода (inferrence), записываемых в виде обыкновенной дроби, где в позиции числителя стоит формализованная фраза ML, а в позиции знаменателя — следствие, которое можно заключить, если фраза корректна.
Определение различает три основные фазы в языке[85][86]: разбор (parsing), выработка (elaboration) и вычисление (evaluation). Выработка относится к статической семантике; вычисление — к динамической. Но вычисление здесь не следует путать с исполнением (execution): SML является языком, основанным на выражениях (expression-based language), и получение результата от применения функции ко всем аргументам называется исполнением (execution), а «вычисление функции» означает построение определения её самой. Следует также обратить внимание, что поддержка каррирования в языке означает представление всех функций замыканиями, а это, в свою очередь, означает, что использовать термин «вызов функции» некорректно. Вместо вызова следует говорить о применении функции (function application) — функция просто не может быть вызвана, пока не получит все аргументы; частичное применение функции означает вычисление новой функции (нового замыкания). Для каждого из слоёв языка (Ядро, Модули, Программы) отдельно описывается статическая и динамическая семантика, то есть этапы разбора, выработки и вычисления.
Конкретная реализация языка не обязана проводить все эти различия, они несут лишь формальный характер[86]. Фактически, единственная реализация, которая стремится строго их соблюдать — это HaMLet . В частности, выработка без вычисления означает традиционное понятие о компиляции.
Вычисление каждого определения по ходу программы меняет состояние глобального окружения (top-level environment), называемого базисом. Формально, исполнение программы представляет собой вычисление нового базиса как суммы начального базиса и определений программы. Стандартная библиотека в SML представляет собой «базис по умолчанию», доступный всякой программе от её начала, и потому называется просто Базисом. Само Определение содержит только начальный базис (initial basis), содержащий минимально необходимые определения; более обширный Базис был стандартизирован много позже, пройдя длительную отработку на практике .
Семантика Харпера — Стоуна
[править | править код]Семантика Харпера — Стоуна (сокращённо «семантика Х-С», англ. HS semantics) представляет собой интерпретацию SML в типизированной системе (typed framework). Семантика SML по Х-С определяется через выработку внешнего языка SML во внутренний язык, представляющий собой явно типизированное лямбда-исчисление, и, таким образом, служит теоретико-типовым обоснованием языка. Эта интерпретация может рассматриваться как альтернатива Определению , формализующая «статические семантические объекты» через выражения типизированного лямбда-исчисления; а также как декларативное описание правил выработки для компиляторов, управляемых типами (англ. type-directed compilers), таких как TILT или SML/NJ . Фактически, фронт-енд компилятора TILT воплощает эту семантику, хотя он был разработан на несколько лет раньше.[87][88][89]
Внутренний язык основан на языке XML Харпера — Митчела, но имеет более обширный набор примитивов и более выразительную систему модулей, основанную на просвечивающих суммах Харпера — Лилибриджа. Этот язык пригоден для выработки многих других языков, семантика которых основана на лямбда-исчислении, таких как Haskell и Scheme.
Применение этого подхода заложено в проект successor ML. При этом, изменения в языке, не влияющие на внутренний язык, рассматриваются как кратковременная перспектива (англ. short-term), а требующие его изменения — как долговременная перспектива (англ. long-term).
Критика и сравнение с альтернативами
[править | править код]Этот раздел не завершён. |
Разработчики SML изначально установили самую высокую планку требований качества для языка, так что и порог критики располагается намного выше, чем у большинства промышленных языков. Упоминания о недостатках языка SML встречаются в официальной печати так же часто, как и языка C++, и много чаще большинства других языков, но причина вовсе не в негативном отношении к SML — напротив, всякая критика SML производится с очень тёплым отношением к нему. Даже педантичный разбор недостатков SML обычно сопровождается его описанием как «изумительного языка, единственного серьёзного из существующих»[90]. Иначе говоря, исследователи досконально копаются в недостатках, подразумевая, что даже с их учётом SML оказывается более предпочтителен для применения в гигантских наукоёмких проектах, чем многие более популярные языки, и желая довести SML до совершенства.
Основной проблемой для разработчика на SML на сегодняшний день является скудный уровень развития окружения (особенно IDE) и библиотечных наработок.
Безопасность SML означает оверхед на арифметику: из-за требования, что всякая операция должна иметь идентичное поведение на любой платформе, контроль переполнения, деления на ноль и т. п. являются неотъемлемыми компонентами всякой арифметической операции. Это делает язык неэффективным выбором для задач числодробилки, особенно для конвейерных архитектур[91].
OCaml является ближайшим родственником SML, отделившимся от него ещё до стандартизации. OCaml настолько шире развит, что его иногда шутливо называют «SML++». В массовом программировании OCaml существенно опережает SML по популярности; в академических кругах SML значительно чаще является объектом научных изысканий. Ведущий разработчик OCaml Ксавье Леруа является членом совета по successor ML.
OCaml имеет единственную реализацию, включающую два компилятора (в байт-код и в натив), совместимых почти идентично, которая непрерывно эволюционирует, предлагая не только всё лучшее окружение, но и всё более мощные семантические возможности. SML имеет множество реализаций различной направленности, следующих единому Определению языка и Базисной библиотеки, и иногда предлагающих дополнительные возможности.
Важнейшие отличия состоят в семантике эквивалентности типов. Во-первых, в SML функторы являются порождающими, а в OCaml — аппликативными (см. эквивалентность типов в языке модулей ML). Во-вторых, OCaml не поддерживает переменные типа, допускающего проверку на равенство (equality type variable): операция проверки на равенство принимает объекты любых типов, но порождает исключение, если они несовместимы.
OCaml современных версий включает семантические возможности, доступные лишь по отдельности в некоторых расширениях SML, например:
- рядный полиморфизм записей и вариантов. Диалект SML# расширяет SML более эффективным и выразительным полиморфизмом записей в модели Охори. Проект развития SML (successor ML) предусматривает обязательную поддержку расширяемых записей (но конкретное исчисление ещё не выбрано).
- модули высшего порядка и другие доработки языка модулей. Поддерживается многими компиляторами SML (но семантика варьируется).
- первоклассные модули в форме пакетов. Диалект Alice ML поддерживает не только сами пакеты, но и их динамическую загрузку и распределение по гетерогенным вычислительным системам с возможностью сериализации.
Haskell является наследником ML/SML (в этом смысле обычно не проводится принципиальных различий между ML и SML). Оба языка основаны на системе типов Хиндли — Милнера, включая выведение типов, из чего следует масса общих черт[95] (первоклассные функции, типобезопасный параметрический полиморфизм, алгебраические типы данных и сопоставление с образцом на них).
Среди ключевых отличий можно назвать[95][96][97][98][99][68][100]:
- SML (как и OCaml) предоставляет возможность полной абстракции типов посредством тёмного (англ. opaque) сопоставления сигнатур в языке модулей. Это обеспечивает возможность использовать сколь угодно высокоуровневую функциональность в качестве примитивной для реализации функциональности ещё более высокого уровня[16]. Haskell не поддерживает абстракцию типа при экспорте из модуля (только сокрытие его конструкторов), что снижает коэффициент повторного использования и затрудняет решение некоторых задач[98].
- Haskell является чистым, т.е. не имеет эффектов, и для моделирования изменяемого состояния использует монады, тогда как SML непосредственно поддерживает мутабельные структуры данных (ссылки и массивы) и управляющие эффекты (исключения и циклы).
- Haskell местами отклоняется от доказуемой надёжности.
- Haskell является ленивым, т.е. основан на вызове по необходимости, и как следствие, использует нестрогое определение функций, что существенно влияет как на выразительные возможности, так и на процесс изучения языка. SML является строгим (энергичным), т.е. основан на вызове по значению, но позволяет легко эмулировать ленивость различной степени и различной эффективности[101].
- Поддержка крупномасштабного программирования[англ.] в Haskell обеспечивается за счёт монад и классов типов. SML гордится уникальным языком модулей. Вопрос о том, какая из систем лучше, является темой горячих споров (см. критика языка модулей и реализация идиом Хаскела в SML).
- В Haskell функции (включая функции над типами), как правило, каррированные. В SML многие библиотечные функции определены над кортежами и записями, а конструкторы типов вообще не могут быть каррированными. Это влияет не только на синтаксис, но и на некоторые идиомы и стереотипы. В частности, для функций свёртки в этих языках используется разный порядок следования аргументов, и более того, чаще применяются разные функции свёртки: в SML предпочтительна свёртка налево как допускающая хвостовую оптимизацию, а в Haskell предпочтительна свёртка направо как допускающая работу над псевдобесконечными списками.
- Система типов Haskell развита значительно дальше: поддерживаются конструкторы типов высшего порядка и, соответственно, различаются их рода́; опционально поддерживаются полиморфизм 2-го и высших рангов, полиморфная рекурсия и даже импредикативный полиморфизм. SML допускает только полиморфизм 1 ранга (пренексный), только унарные конструкторы типов (как следствие, рода́ не включены в Определение, но упоминаются в Комментариях[102] и присутствуют явным образом в семантике Х-С ) и требует предикативности для типов модулей[103]. Эти ограничения в некоторых случаях можно обойти применением эта-расширения ; они носят чисто исторический характер и исчезнут в ML следующего поколения.
- Haskell наделяет списки дополнительными привилегиями: поддерживается синтаксический сахар в слое типов (запись «
[a]
» тождественна «List a
») и списковые включения.
История, философия, терминология
[править | править код]
Формальная семантика SML ориентирована на интерпретацию, однако большинство его реализаций является компиляторами (в том числе интерактивными компиляторами), некоторые из которых уверенно соперничают по эффективности с языком Си, так как язык хорошо поддаётся глобальному анализу. По той же причине SML может компилироваться в исходный код на других языках высокого или среднего уровня — например, существуют компиляторы из SML в Си и Ada.
В основе языка лежит сильная статическая полиморфная типизация, которая не только обеспечивает верификацию программ на этапе компиляции, но и жёстко обособляет мутабельность, что само по себе повышает потенциал к автоматической оптимизации программ — в частности, упрощает реализацию сборщика мусора[104].
Первая версия ML была представлена миру в 1974 году в роли мета-языка для построения интерактивных доказательств в составе системы Edinburgh LCF (Logic for Computable Functions)[англ.][2]. Её реализовали Малькольм Ньюи, Локвуд Моррис и Робин Милнер на платформе DEC10. Первая реализация была крайне неэффективной, так как конструкции ML транслировались в Lisp, который затем интерпретировался[105]. Первое полное описание ML как компонента LCF издано в 1979 году[2].
Около 1980 года Лука Карделли[англ.] реализовал первый компилятор Vax ML, дополнив ML некоторыми своими идеями. Вскоре Карделли портировал Vax ML на Unix, используя Berkley Pascal. Среда выполнения была переписана на Си, но большая часть компилятора оставалась на Паскале. Работа Карделли вдохновила Милнера на создание SML как самостоятельного языка общего назначения, и они начали совместную работу в Эдинбурге, результатом чего стал компилятор Edinburgh ML , выпущенный в 1984 году. В процессе этой работы Майк Гордон придумал ссылочные типы и предложил их Луи Дамасу, который позже защитил на них диссертацию[106]. Одновременно велось сотрудничество Кэмбриджа с INRIA. Жерар Хью из INRIA портировал ML на Maclisp под Multics. INRIA разработали собственный диалект ML, названный Caml, и впоследствии развившийся в OCaml . Лоуренс Полсон[англ.] оптимизировал Edinburgh ML , так что код на ML стал работать в 4-5 раз быстрее. Вскоре после этого Дэвид Мэтьюз разработал язык Poly на основе ML. Дальнейшая работа в этом направлении привела к созданию среды Poly/ML . В 1986 Дэвид МакКуин сформулировал язык модулей ML, и к работе подключился Эндрю Аппель[англ.]. Совместно они начали вести работу над компилятором SML/NJ[англ.], который служил одновременно исследовательской платформой для развития языка и первым промышленным оптимизирующим компилятором. Многие из реализаций языка были первоначально разработаны с использованием SML/NJ[англ.] и затем раскручены.
С опытом крупномасштабных разработок был обнаружен ряд недочётов в Определении языка от 1990 года[3], но рамки ревизии исключают потерю обратной совместимости (коды адаптируются косметически, без необходимости переписывания с нуля). В 2004 году была опубликована спецификация на состав Базисной библиотеки (черновик спецификации датируется 1996 годом). Другие недостатки были устранены в других языках: ML породил целое семейство Х-М-типизированных языков. Эти языки завоевали популярность на задаче разработке языков и часто определяются как «DSL для денотационной семантики[англ.]». Исследователи, занимавшиеся развитием и использованием SML на протяжении почти трёх десятилетий, к концу XX века сформировали сообщество по созданию нового языка — successor ML.
. Часть недостатков была устранена в Ревизии Определения от 1997 годаФактически, SML не был первым в семействе после собственно LCF/ML — ему предшествовали такие языки как Cardelli ML и Hope[9]. Французы поддерживают собственный диалект — Caml/OCaml[12]. Тем не менее, говоря «ML», многие подразумевают «SML»[107], и даже пишут через дробь: «ML/SML»[82].
Изучение
[править | править код]Наиболее рекомендуемым[108][109][110][111][112][113] учебником по SML является книга Лоуренса Полсона[англ.] (автора системы HOL[англ.]) «ML for the Working Programmer»[107].
Для первоначального ознакомления с языком может быть полезен краткий (несколько десятков страниц) курс Роберта Харпера[англ.] «Introduction to Standard ML» (доступный в русском переводе[114]), который он использовал для преподавания языка и за следующие два десятилетия расширил до более крупного учебника[115].
Учебным руководством по использованию стандартной библиотеки языка, предполагающим его базовое знание, служит книга Рикардо Пуцеллы[30].
В числе других учебников можно назвать книги Гилмора[116], Ульмана[117], Шипмана[118], онлайн-книгу Камминга[119].
Среди руководств по профессиональному использованию языка можно выделить книгу Эндрю Аппеля[англ.] (ведущего разработчика SML/NJ[англ.]) «Modern compiler implementation in ML»[120] (у этой книги есть две сестры-близняшки: «Modern compiler implementation in Java» и «Modern compiler implementation in C», эквивалентные по структуре, но использующие другие языки для воплощения излагаемых методов). Имеется также масса статей, издаваемых в таких журналах, как JFP, «ML workshop» и др.[121][122]
Применение
[править | править код]SML, наряду с OCaml, служит первым языком преподавания обучения программированию во многих университетах мира. Среди аппликативных языков они имеют, вероятно, самый низкий собственный порог вхождения.
Значительная часть существующих кодов на SML представляет собой либо реализацию его же компиляторов, либо системы автоматического доказательства, такие как HOL[англ.], Twelf[англ.] и Isabelle (система автоматического доказательства теорем). Все они свободны и открыты.
Тем не менее, существуют и более «приземлённые», в том числе проприетарные продукты[123].
Примечания
[править | править код]- ↑ SML'84, 1984.
- ↑ 1 2 3 4 SML'90, 1990.
- ↑ 1 2 3 SML'97, 1997.
- ↑ SML'90, 1990, E. Appendix: The Development of ML, с. 81—83.
- ↑ 1 2 3 Tarditi et al, "No Assembly Required", 1990.
- ↑ 1 2 Tolmach, Oliva, "From ML to Ada", 1993.
- ↑ 1 2 Commentary on SML, 1991, с. V.
- ↑ 1 2 Pucella, "Notes on SML/NJ", 2001, с. 1.
- ↑ 1 2 3 4 MacQueen, "Reflections on SML", 1992.
- ↑ StandardML description in MLton compiler guide . Дата обращения: 14 августа 2016. Архивировано 25 августа 2016 года.
- ↑ 1 2 ML2000 Preliminary Design, 1999.
- ↑ 1 2 Paulson, "ML for the Working Programmer", 1996, с. 12.
- ↑ Paulson, "ML for the Working Programmer", 1996, с. 2.
- ↑ Rossberg, "1ML", 2015.
- ↑ Harper-Stone '99, 1999.
- ↑ 1 2 Paulson, "ML for the Working Programmer", 1996, 4.13 Tree-based data structures, с. 148—149.
- ↑ 1 2 OOP in SML.
- ↑ MacQueen, "Reflections on SML", 1992, с. 2.
- ↑ Commentary on SML, 1991, с. 15.
- ↑ Paulson, "ML for the Working Programmer", 1996, Imperative Programming in ML, с. 313.
- ↑ MacQueen, "Reflections on SML", 1992, с. 3.
- ↑ Paulson, "ML for the Working Programmer", 1996, с. 1.
- ↑ 1 2 Appel, "A Critique of Standard ML", 1992, Lack of macros, с. 9.
- ↑ 1 2 VandenBerghe, "Why ML/OCaml are good for writing compilers", 1998.
- ↑ Paulson, "ML for the Working Programmer", 1996, 7.8 Testing the queue structures, с. 274.
- ↑ MacQueen, "Reflections on SML", 1992, с. 6.
- ↑ 1 2 Paulson, "ML for the Working Programmer", 1996, 2.3 Identifiers in Standard ML, с. 21.
- ↑ Paulson, "ML for the Working Programmer", 1996, с. 13.
- ↑ SML Basis, 2004.
- ↑ 1 2 Pucella, "Notes on SML/NJ", 2001.
- ↑ Pucella, "Notes on SML/NJ", 2001, 4.3. More on strings, с. 89—92.
- ↑ Pucella, "Notes on SML/NJ", 2001, 4.3. More on strings, с. 90.
- ↑ 1 2 Standard ML Portability.
- ↑ сайт проекта SML/NJ . Дата обращения: 14 августа 2016. Архивировано 1 мая 2020 года.
- ↑ Deviations of SML/NJ from The Definition of SML'97 (Revised) . Дата обращения: 14 августа 2016. Архивировано 4 апреля 2016 года.
- ↑ SML/NJ: Object Language Embedding with Quote/Antiquote . Дата обращения: 14 августа 2016. Архивировано 19 июня 2016 года.
- ↑ Slind, "Language embedding in SML/NJ", 1991.
- ↑ сайт проекта Poly/ML Архивная копия от 27 июня 2020 на Wayback Machine
- ↑ сайт проекта ML Kit . Дата обращения: 14 августа 2016. Архивировано из оригинала 19 июля 2016 года.
- ↑ 1 2 сайт проекта Manticore . Дата обращения: 14 августа 2016. Архивировано 8 августа 2016 года.
- ↑ сайт проекта CakeML . Дата обращения: 14 августа 2016. Архивировано 14 сентября 2020 года.
- ↑ конференция sml-evolution: Rober Harper, 30.10.2006.
- ↑ Shao, "FLINT/ML Compiler", 1997.
- ↑ сайт проекта MoscowML . Дата обращения: 14 августа 2016. Архивировано 11 января 2016 года.
- ↑ 1 2 MLton Performance.
- ↑ сайт проекта SML.NET . Дата обращения: 14 августа 2016. Архивировано 29 января 2016 года.
- ↑ сайт проекта SMLtoJs . Дата обращения: 14 августа 2016. Архивировано из оригинала 14 сентября 2016 года.
- ↑ страница SMLonline . Дата обращения: 14 августа 2016. Архивировано из оригинала 2 октября 2016 года.
- ↑ исходные коды sml2c . Дата обращения: 14 августа 2016. Архивировано 28 августа 2018 года.
- ↑ From ML to Ada - description in MLton compiler guide . Дата обращения: 16 сентября 2016. Архивировано из оригинала 23 сентября 2016 года.
- ↑ Koser, Larsen, Vaughan, "SML2Java", 2003.
- ↑ сайт проекта HaMLet . Дата обращения: 14 августа 2016. Архивировано 14 октября 2016 года.
- ↑ сайт проекта Isabelle/ML . Дата обращения: 26 августа 2016. Архивировано 30 августа 2020 года.
- ↑ сайт проекта Poplog . Дата обращения: 26 августа 2016. Архивировано 18 августа 2016 года.
- ↑ Проект Standard ML на сайте GitHub
- ↑ сайт проекта SML# . Дата обращения: 14 августа 2016. Архивировано 8 июня 2020 года.
- ↑ сайт проекта Mythril . Дата обращения: 14 августа 2016. Архивировано 28 июня 2009 года.
- ↑ Taha et al, "Macros as Multi-Stage Computations", 2001.
- ↑ Pucella, "Notes on SML/NJ", 2001, Chapter 6. The Compilation Manager, с. 157.
- ↑ eXene — multi-threaded X Window System toolkit written in ConcurrentML . Дата обращения: 14 августа 2016. Архивировано 22 февраля 2012 года.
- ↑ Huelsbergen, "Portable C Interface for SML", 1996.
- ↑ Chris Cannam, "Why was OCaml faster?".
- ↑ Blume, "No-Longer-Foreign", 2001.
- ↑ Standard ML Style Guide (from MLton guide) . Дата обращения: 14 августа 2016. Архивировано 27 августа 2016 года.
- ↑ Appel, "A Critique of Standard ML", 1992, Misspelled constructors, с. 12.
- ↑ Harper, "Intro to SML", 1986, с. 5.
- ↑ «EtaExpansion» technique (from MLton Guide) . Дата обращения: 6 сентября 2016. Архивировано 10 сентября 2016 года.
- ↑ 1 2 Peyton-Jones, "retrospective on Haskell", 2003.
- ↑ Type-indexed values (from MLton Guide) . Дата обращения: 26 августа 2016. Архивировано 21 апреля 2016 года.
- ↑ «Fold» technique (from MLton Guide) . Дата обращения: 24 августа 2016. Архивировано 26 сентября 2016 года.
- ↑ Shipman, "Unix Programming with SML", 2001, с. 31.
- ↑ Paulson, "ML for the Working Programmer", 1996, 8.9 Text processing examples, с. 348—350.
- ↑ 1 2 Paulson, "ML for the Working Programmer", 1996, 1.5 The efficiency of functional programming, с. 9.
- ↑ 1 2 3 Appel, "A Critique of Standard ML", 1992.
- ↑ Paulson, "ML for the Working Programmer", 1996, с. 108.
- ↑ Commentary on SML, 1991, Aims of the Commentary, с. vii.
- ↑ Commentary on SML, 1991.
- ↑ about The Definition Of Standard ML in MLton guide (недоступная ссылка)
- ↑ Kahrs, 1993.
- ↑ Kahrs, 1996.
- ↑ Defects in SML (from HaMLet manual) . Дата обращения: 6 сентября 2016. Архивировано 4 мая 2016 года.
- ↑ 1 2 sml-family.org.
- ↑ Paulson, "ML for the Working Programmer", 1996, 1.9 ML and the working programmer, с. 16.
- ↑ SML'90, 1990, с. V.
- ↑ SML'90, 1990, с. 1.
- ↑ 1 2 Commentary on SML, 1991, с. 1—3.
- ↑ Harper-Stone '96, 1996.
- ↑ Harper-Stone '97, 1997.
- ↑ Harper-Stone '99, 1999, с. 1—2.
- ↑ 1 2 Rossberg, "Defects in SML Revised", 2001.
- ↑ Harper, "Programming in SML", 2005, 12.1.1 Primitive Exceptions, с. 104.
- ↑ Chris Cannam, "Four MLs (and a Python)".
- ↑ Chlipala, "OCaml vs. SML".
- ↑ Olsson, Rossberg, "SML vs. OCaml".
- ↑ 1 2 Shaw, "ML vs. Haskell", 2012.
- ↑ Dreyer, Harper, "Modular Type Classes", 2007.
- ↑ Yallop, White, "Lightweight higher-kinded polymorphism", 2014.
- ↑ 1 2 Augustsson, "Failed adventure in Haskell Abstraction".
- ↑ Wehr, Chakravarty, "Modules vs. Type Classes", 2008.
- ↑ Harper, "Of Course ML has Monads!".
- ↑ Paulson, "ML for the Working Programmer", 1996, Sequences, or infinite lists, с. 191—201.
- ↑ Commentary on SML, 1991, 3 Dynamic Semantics for the Modules, с. 26.
- ↑ Rossberg, "1ML", 2015, с. 2.
- ↑ Appel, "A Critique of Standard ML", 1992, Efficiency, с. 7—8.
- ↑ Paulson, "ML for the Working Programmer", 1996, с. 11.
- ↑ MacQueen, "Cardelli and Early Evolution of ML", 2014, с. 4.
- ↑ 1 2 Paulson, "ML for the Working Programmer", 1996.
- ↑ Recommended books on SML/NJ compiler page . Дата обращения: 26 августа 2016. Архивировано 19 августа 2016 года.
- ↑ Gilmore, "Programming in SML. Tutorial Introduction", 1997, с. 3.
- ↑ Shipman, "Unix Programming with SML", 2001, с. 455.
- ↑ MacQueen, "Reflections on SML", 1992, с. 1.
- ↑ Pucella, "Notes on SML/NJ", 2001, с. 42.
- ↑ SML Basis on Cambridge University Press — related books . Дата обращения: 19 мая 2022. Архивировано 24 февраля 2021 года.
- ↑ Harper, "Intro to SML", 1986.
- ↑ Harper, "Programming in SML", 2005.
- ↑ Gilmore, "Programming in SML. Tutorial Introduction", 1997.
- ↑ Ullman, "Elements of ML Programming", 1998.
- ↑ Shipman, "Unix Programming with SML", 2001.
- ↑ Cumming, 1995.
- ↑ Appel, "Modern compiler implementation in ML", 1998.
- ↑ Fluet, Pucella, "Phantom Types and Subtyping", 2006.
- ↑ Pucella, "Reactive Programming in SML", 2004.
- ↑ Пользователи Standard ML . Дата обращения: 14 августа 2016. Архивировано 10 сентября 2016 года.
Литература
[править | править код]Стандарты
[править | править код]- Robin Milner. A Proposal for Standard ML. — 1984. — doi:10.1145/800055.802035.
- Robin Milner, Mads Tofte[англ.], Robert Harper[англ.]. The Definition of Standard ML (англ.). — The MIT Press, 1990. — ISBN 0-262-63181-4.
- Robin Milner, Mads Tofte[англ.]. Commentary on Standard ML (англ.). — MIT Press, 1991. — ISBN 0-262-63132-7.
- Robin Milner, Mads Tofte[англ.], Robert Harper[англ.], David MacQueen. The Definition of Standard ML: Revised (англ.). — The MIT Press, 1997. — ISBN 0262631814.
- Emden R. Gansner, John H. Reppy. The Standard ML Basis Library (англ.). — Cambridge University Press, 2004. — 484 p. — ISBN 9780521794787.
- Полная грамматика Standard ML (англ.). (made up by Andreas Rossberg).
Учебники, руководства, справочники, использование
[править | править код]- Роберт Харпер[англ.]. Введение в Стандартный ML. — Carnegie Mellon University, 1986. — 97 с. — ISBN PA 15213-3891.
- Konrad Slind. Object language embedding in Standard ML of New Jersey. — Proceedings of the 2nd ML workshop, Carnegie Mellon University., 1991.
- Andrew Cumming. A Gentle Introduction to ML. — Napier University, Edinburgh, 1995.
- Lawrence C. Paulson[англ.]. ML for the Working Programmer. — 2nd. — Cambridge, Great Britain: Cambridge University Press, 1996. — 492 с. — ISBN 0-521-57050-6 (твёрдый переплёт), 0-521-56543-X (мягкий переплёт).
- Stephen Gilmore. Programming in Standard ML '97: A Tutorial Introduction (англ.). — Laboratory for Foundations of CS, Department of CS, 1997. Архивная копия от 21 июля 2001 на Wayback Machine
- Jeffrey Ullman. Elements of ML Programming (англ.). — Prentice-Hall, 1998. — ISBN 0-13-790387-1.
- Andrew W. Appel. Modern compiler implementation in ML (англ.). — Cambridge, Great Britain: Cambridge University Press, 1998. — 538 p. — ISBN 0-521-58274-1 (hardback), 0-521-60764-7 (paperback).
- Anthony L. Shipman. Unix System Programming with Standard ML (англ.). — 2001.
- Riccardo Pucella. Notes on Programming Standard ML of New Jersey (англ.). — Last revised January 10, 2001. — Cornell University, 2001.
- Bernard Berthomieu. OO Programming Styles in ML. — LAAS Report #2000111, Centre National De La Recherche Scientifique Laboratoire d'Analyse et d'Architecture des Systèmes, 2000.
- Riccardo R. Pucella. Reactive Programming in Standard ML (англ.). — Bell Laboratories, Lucent Technologies, 2004.
- Robert Harper[англ.]. Programming in Standard ML (англ.) / licensed under the Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 United States License. — Draft: ver.1.2 of 11.02.2011. — Carnegie Mellon University, 2005. — 297 p. Архивная копия от 14 сентября 2012 на Wayback Machine
- Matthew Fluet, Riccardo Pucella. Phantom Types and Subtyping (англ.). — JFP, 2006. — общая техника усиления типизации для раннего выявления ошибок (см. также полнотиповое программирование)
История, анализ, критика
[править | править код]- Milner, Morris, Newey. A Logic for Computable Functions with reflexive and polymorphic types // Arc-et-Senans. — Proc. Conference on Proving and Improving Programs, 1975.
- Gordon, Milner, Morris, Newey, Wadsworth. A Metalanguage for Interactive Proof in LCF. — 1977.
- Robin Milner. A Theory of Type Polymorphism in Programming. — Journal of Computer and System Sciences[англ.], 1978. — Т. 17, вып. 3. — С. 348—375. — doi:10.1016/0022-0000(78)90014-4.
- David MacQueen. Structures and parameterisation in a typed functional language. — 1981.
- Robin Milner. How ML evolved. — 1983.
- David MacQueen. Modules for Standard ML. — LFP '84 Proceedings of the 1984 ACM Symposium on LISP and functional programming, 1984. — С. 198—207. — ISBN 0-89791-142-3. — doi:10.1145/800055.802036.
- Andrew W. Appel. A Critique of Standard ML. — Princeton University, revised version of CS-TR-364-92, 1992.
- David MacQueen. Reflections on Standard ML. — AT&T Bell Laboratories, 1992. — doi:10.1.1.104.171.
- Stefan Kahrs. Mistakes and Ambiguities in the Definition of Standard ML. — University of Edinburgh, 1993.
- Andrew Appel, David MacQueen. Separate Compilation for Standard ML (англ.). — SIGPLAN 94-6/94, ACM 0-89791-662-x/94/006, 1994. — doi:10.1.1.14.4810.
- Stefan Kahrs. Mistakes and Ambiguities in the Definition of Standard ML – Addenda (англ.). — University of Edinburgh, 1996. (недоступная ссылка)
- Michael J.C.Gordon. From LCF to HOL: a short history (англ.). — 1996.
- Robert Harper[англ.], Christopher A. Stone. A type-theoretic account of Standard ML // Technical Report CMU-CS-96-136R. — Carnegie Mellon University, 1996.
- Lorenz Huelsbergen. A Portable C Interface for Standard ML of New Jersey. — 1996.
- Robert Harper[англ.], Christopher A. Stone. An interpretation of Standard ML in type theory // Technical Report CMU-CS-97-147. — Carnegie Mellon University, 1997.
- Zhong Shao. An Overview of the FLINT/ML Compiler. — In Proc. ACM SIGPLAN Workshop on Types in Compilation (TIC), 1997.
- Zhe Yang. Encoding Types in ML-like Languages. — New York University, (c) ACM, 1998. — doi:10.1.1.127.2311.
- Dwight VandenBerghe. Why ML/OCaml are good for writing compilers. — 1998. Архивировано 20 августа 2016 года.
- The ML2000 Working Group. Principles and a Preliminary Design for ML2000 (англ.). — 1999.
- Robert Harper[англ.], Christopher A. Stone. A type-theoretic interpretation of Standard ML // In Proof, Language, and Interaction: Essays in Honor of Robin Milner. — MIT Press, 1999.
- Andreas Rossberg. Defects in the Revised Definition of Standard ML. — Universitat des Saarlandes, 2001.
- Matthias Blume. No-Longer-Foreign - Teaching an ML compiler to speak C natively (англ.) // Theoretical Computer Science[англ.] : PDF. — Lucent Technologies, Bell Laboratories, 2001. — Vol. 59, no. No. 1.
- Simon Peyton Jones. Wearing the hair shirt: a retrospective on Haskell. — Invited talk at POPL, 2003.
- Adam Shaw. A general comparison of Haskell and ML. — 2012.
- Andreas Rossberg, Claudio Russo, Derek Dreyer. F-ing Modules (англ.). — TLDI, 2010.
- David MacQueen. Luca Cardelli and the Early Evolution of ML. — 2014.
- Andreas Rossberg. 1ML – Core and Modules United (F-ing First-class Modules) (англ.). — ICFP, 2015.
- David MacQueen. The History of Standard ML: Ideas, Principles, Culture. — 2015.
Прочее
[править | править код]- David Tarditi, Peter Lee, Anurag Acharya. No Assembly Required - Compiling Standard ML to C. — 1990.
- Andrew Tolmach and Dino Oliva. From ML to Ada: Strongly-typed Language Interoperability via Source Translation. — JFP, Cambridge University Press, 1993.
- Steven E. Ganz, Amr Sabry, Walid Taha. Macros as Multi-Stage Computations: Type-Safe, Generative, Binding Macros in MacroML. — International Conference on Functional Programming, ACM Press, 2001. Архивировано 23 сентября 2015 года.
- Justin Koser, Haakon Larsen, and Jeffrey A. Vaughan. SML2Java: A Source to Source Translator. — 2003.
- Derek Dreyer, Robert Harper[англ.]. Modular Type Classes (англ.). — ACM SIGPLAN, 2007.
- Stefan Wehr, Manuel M.T.Chakravarty. ML Modules and Haskell Type Classes: A Constructive Comparison. — APLAS, Springer-Verlag, LNCS, 2008.
- Robert Harper[англ.]. Of Course ML has Monads! (англ.) (2011).
- Jeremy Yallop, Leo White. Lightweight higher-kinded polymorphism. — Proceedings of the Functional and Logic Programming, 2014.
- 6.1 The Folks Who Made It Happen (англ.).
Ссылки
[править | править код]- Standard ML official website (англ.).
- MLton Performance (англ.) (2005).
- Jens Olsson, Andreas Rossberg. Standard ML and Objective Caml, Side by Side (англ.).
- Adam Chlipala. Comparing Objective Caml and Standard ML (англ.).
- Chris Cannam. SML and OCaml: So, why was the OCaml faster? (англ.).
- Chris Cannam. Four MLs (and a Python) (англ.).