Standard ML ( SML ) — это универсальный , высокоуровневый , модульный , функциональный язык программирования с проверкой типов во время компиляции и выводом типов . Он популярен для написания компиляторов , исследования языков программирования и разработки средств доказательства теорем .
Стандартный ML — это современный диалект ML , языка, используемого в проекте доказательства теорем Логика для вычислимых функций (LCF). Он отличается от широко используемых языков тем, что имеет формальную спецификацию , заданную в виде правил типизации и операционной семантики в Определении стандартного ML . [5]
Standard ML — это функциональный язык программирования с некоторыми нечистыми функциями. Программы, написанные на Standard ML, состоят из выражений , в отличие от операторов или команд, хотя некоторые выражения типа unit оцениваются только на предмет их побочных эффектов .
Как и все функциональные языки, ключевой особенностью Standard ML является функция , которая используется для абстракции. Функция факториала может быть выражена следующим образом:
забавный факториал n = если n = 0 , то 1 , иначе n * факториал ( n - 1 )Компилятор SML должен вывести статический тип без аннотаций типа, предоставленных пользователем. Он должен вывести, что используется только с целочисленными выражениями, и, следовательно, сам должен быть целым числом, и что все терминальные выражения являются целочисленными выражениями.val factorial : int -> intn
Эту же функцию можно выразить с помощью определений клаузальных функций, где условные операторы if - then - else заменяются шаблонами факториальной функции, вычисляемой для определенных значений:
забавный факториал 0 = 1 | факториал n = n * факториал ( n - 1 )или итеративно:
fun factorial n = let val i = ref n и acc = ref 1 in while !i > 0 do ( acc := !acc * !i ; i := !i - 1 ); !acc endили как лямбда-функция:
val rec факториал = fn 0 => 1 | n => n * факториал ( n - 1 )Здесь ключевое слово valвводит привязку идентификатора к значению, fnвводит анонимную функцию и recпозволяет определению быть самоссылающимся.
Инкапсуляция сохраняющего инварианты хвостового рекурсивного плотного цикла с одним или несколькими параметрами накопителя внутри внешней функции, свободной от инвариантов, как показано здесь, является распространенной идиомой в стандартном ML.
Используя локальную функцию, ее можно переписать в более эффективном стиле хвостовой рекурсии:
локальный цикл веселья ( 0 , acc ) = acc | цикл ( m , acc ) = цикл ( m - 1 , m * acc ) в факториале веселья n = цикл ( n , 1 ) конец Синоним типа определяется ключевым словом type. Здесь представлен синоним типа для точек на плоскости , а также функции, вычисляющие расстояния между двумя точками и площадь треугольника с заданными углами по формуле Герона . (Эти определения будут использоваться в последующих примерах).
тип loc = реальный * реальныйзабавный квадрат ( x : действительный ) = x * xзабавное расстояние ( x , y ) ( x' , y' ) = Математика . квадрат ( квадрат ( x' - x ) + квадрат ( 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 в Math . sqrt ( s * ( s - x ) * ( s - y ) * ( s - z )) endСтандартный ML обеспечивает сильную поддержку алгебраических типов данных (ADT). Тип данных можно рассматривать как непересекающееся объединение кортежей (или «сумму произведений»). Их легко определить и использовать, в основном из-за сопоставления с образцом и проверки исчерпывающей полноты и избыточности образов большинства реализаций стандартного ML .
В объектно-ориентированных языках программирования непересекающееся объединение может быть выражено в виде иерархий классов . Однако, в отличие от иерархий классов , АТД являются закрытыми . Таким образом, расширяемость АТД ортогональна расширяемости иерархий классов. Иерархии классов могут быть расширены новыми подклассами, реализующими тот же интерфейс, в то время как функции АТД могут быть расширены для фиксированного набора конструкторов. См. проблему выражения .
Тип данных определяется с помощью ключевого слова datatype, например:
тип данных shape = Круг loc * real (* центр и радиус *) | Квадрат loc * real (* верхний левый угол и длина стороны ; выровнен по осям *) | Треугольник loc * loc * loc ( * углы *) Обратите внимание, что синоним типа не может быть рекурсивным; типы данных необходимы для определения рекурсивных конструкторов. (В данном примере это не рассматривается.)
Шаблоны сопоставляются в том порядке, в котором они определены. Программисты на C могут использовать помеченные объединения , диспетчеризируя значения тегов, чтобы делать то, что ML делает с типами данных и сопоставлением шаблонов. Тем не менее, хотя программа на C, украшенная соответствующими проверками, будет в некотором смысле такой же надежной, как и соответствующая программа ML, эти проверки по необходимости будут динамическими; статические проверки ML предоставляют надежные гарантии правильности программы во время компиляции.
Аргументы функции можно определить как шаблоны следующим образом:
забавная площадь ( Круг (_, r )) = Математика . пи * квадрат r | площадь ( Квадрат (_, s )) = квадрат s | площадь ( Треугольник p ) = цапля p (* см. выше *)Так называемая «клаузальная форма» определения функции, в которой аргументы определяются как шаблоны, является всего лишь синтаксическим сахаром для выражения case:
забавная форма области = случай формы Круг (_, r ) => Математика . пи * квадрат r | Квадрат (_, s ) => квадрат s | Треугольник p = > цапля p Проверка на полноту шаблона гарантирует, что каждый конструктор типа данных соответствует хотя бы одному шаблону.
Следующая схема не является исчерпывающей:
центр веселья ( круг ( c , _)) = c | центр ( квадрат (( x , y ), s )) = ( x + s / 2.0 , y + s / 2.0 )TriangleВ функции нет шаблона для case center. Компилятор выдаст предупреждение о том, что выражение case не является исчерпывающим, и если Triangleв эту функцию во время выполнения будет передано a, будет вызвано исключение.exception Match
Шаблон во втором предложении следующей (бессмысленной) функции избыточен:
забава f ( Круг (( x , y ), r )) = x + y | f ( Круг _) = 1.0 | f _ = 0.0Любое значение, которое будет соответствовать шаблону во втором предложении, будет также соответствовать шаблону в первом предложении, поэтому второе предложение недостижимо. Следовательно, это определение в целом демонстрирует избыточность и вызывает предупреждение во время компиляции.
Следующее определение функции является исчерпывающим и не является избыточным:
val hasCorners = fn ( Circle _) => false | _ => trueЕсли управление проходит мимо первого шаблона ( Circle), мы знаем, что форма должна быть либо a , Squareлибо a Triangle. В любом из этих случаев мы знаем, что у формы есть углы, поэтому мы можем вернуться, trueне различая фактическую форму.
Функции могут использовать функции в качестве аргументов:
забавная карта f ( x , y ) = ( f x , f y )Функции могут создавать функции как возвращаемые значения:
константа веселья k = ( fn _ => k )Функции также могут как потреблять, так и производить функции:
весело составить ( f , g ) = ( fn x => f ( g x ))Функция List.mapиз базовой библиотеки является одной из наиболее часто используемых функций высшего порядка в Standard ML:
забавная карта _ [] = [] | карта f ( x :: xs ) = f x :: карта f xsБолее эффективная реализация с хвостовой рекурсией List.foldl:
fun map f = List.rev o List.foldl ( fn ( x , acc ) = > f x :: acc ) [ ] Исключения вызываются ключевым словом raiseи обрабатываются конструкцией сопоставления с образцом handle. Система исключений может реализовать нелокальный выход; этот метод оптимизации подходит для функций, подобных следующим.
локальное исключение Zero ; val p = fn ( 0 , _) => raise Zero | ( a , b ) = > a * b in fun prod xs = List.foldl p 1 xs handle Zero = > 0 end При возникновении исключения управление полностью покидает функцию . Рассмотрим альтернативу: будет возвращено значение 0, оно будет умножено на следующее целое число в списке, будет возвращено результирующее значение (неизбежно 0) и т. д. Возникновение исключения позволяет управлению пропустить всю цепочку кадров и избежать связанных вычислений. Обратите внимание на использование подчеркивания ( ) в качестве шаблона подстановки.exception ZeroList.foldl_
Такую же оптимизацию можно получить с помощью хвостового вызова .
локальная забава p a ( 0 :: _) = 0 | p a ( x :: xs ) = p ( a * x ) xs | p a [] = a in val prod = p 1 endРасширенная система модулей Standard ML позволяет разлагать программы на иерархически организованные структуры логически связанных определений типов и значений. Модули обеспечивают не только управление пространством имен, но и абстракцию, в том смысле, что они позволяют определять абстрактные типы данных . Три основные синтаксические конструкции составляют систему модулей: сигнатуры, структуры и функторы.
Сигнатура — это интерфейс , обычно рассматриваемый как тип для структуры; он определяет имена всех сущностей, предоставляемых структурой, арность каждого компонента типа, тип каждого компонента значения и сигнатуру каждой подструктуры. Определения компонентов типа являются необязательными; компоненты типа, определения которых скрыты, являются абстрактными типами .
Например, подпись для очереди может быть такой:
signature QUEUE = sig type 'a queue exception QueueError ; val empty : 'a queue val isEmpty : 'a queue -> bool val singleton : 'a -> 'a queue val fromList : 'a list -> 'a queue val insert : 'a * 'a queue -> 'a queue val peek : 'a queue -> 'a val remove : 'a queue -> 'a * 'a queue endЭта сигнатура описывает модуль, который предоставляет полиморфный тип , и значения, которые определяют основные операции над очередями.'a queueexception QueueError
Структура — это модуль ; она состоит из набора типов, исключений, значений и структур (называемых подструктурами ), упакованных вместе в логическую единицу.
Структуру очереди можно реализовать следующим образом:
структура TwoListQueue :> QUEUE = тип структуры ' очередь = ' список * ' список исключение QueueError ; значение пусто = ([], []) забава isEmpty ([], []) = истина | isEmpty _ = ложь забавный синглтон a = ([], [ a ]) веселье из списка a = ([], a ) забавная вставка ( a , ([], [])) = синглтон a | вставка ( a , ( ins , outs )) = ( a :: ins , outs ) fun peek (_, []) = raise QueueError | peek ( ins , outs ) = List . hd outs забавно удалить (_, []) = вызвать QueueError | удалить ( ins , [ a ]) = ( a , ([], Список . rev ins )) | удалить ( ins , a :: outs ) = ( a , ( ins , outs )) конецЭто определение объявляет, что реализует . Кроме того, непрозрачное приписывание , обозначенное как , утверждает, что любые типы, которые не определены в сигнатуре (т.е. ), должны быть абстрактными, что означает, что определение очереди как пары списков не видно за пределами модуля. Структура реализует все определения в сигнатуре.structure TwoListQueuesignature QUEUE:>type 'a queue
Доступ к типам и значениям в структуре можно получить с помощью «точечной нотации»:
значение q : string TwoListQueue.queue = TwoListQueue.empty значение q ' = TwoListQueue.insert ( Real.toString Math.pi , q ) Функтор — это функция из структур в структуры; то есть функтор принимает один или несколько аргументов, которые обычно являются структурами заданной сигнатуры, и производит структуру в качестве своего результата. Функторы используются для реализации общих структур данных и алгоритмов.
Один популярный алгоритм [6] для поиска в ширину деревьев использует очереди. Вот версия этого алгоритма, параметризованная по абстрактной структуре очереди:
(* по Окасаки, ICFP, 2000 *) функтор BFS ( Q : QUEUE ) = struct datatype 'a tree = E | T of 'a * 'a tree * 'a tree локальная функция bfsQ q = if Q . isEmpty q then [] else search ( Q . remove q ) и search ( E , q ) = bfsQ q | search ( T ( x , l , r ), q ) = x :: bfsQ ( insert ( insert q l ) r ) и insert q a = Q . insert ( a , q ) in fun bfs t = bfsQ ( Q . singleton t ) end endструктура QueueBFS = BFS ( TwoListQueue )В пределах представление очереди не видно. Более конкретно, нет способа выбрать первый список в двухсписочной очереди, если это действительно используемое представление. Этот механизм абстракции данных делает поиск в ширину действительно независимым от реализации очереди. Это в целом желательно; в этом случае структура очереди может безопасно поддерживать любые логические инварианты, от которых зависит ее корректность, за пуленепробиваемой стеной абстракции.functor BFS
Фрагменты кода SML проще всего изучать, вводя их в интерактивный файл верхнего уровня .
Ниже представлена программа «Hello, World!» :
Сортировку вставкой (по возрастанию) можно кратко выразить следующим образом:int list
забавная вставка ( x , []) = [ x ] | вставка ( x , h :: t ) = сортировка x ( h , t ) и сортировка x ( h , t ) = если x < h то [ x , h ] @ t иначе h :: вставка ( x , t ) val вставка сортировка = Список . foldl вставка []Здесь классический алгоритм mergesort реализован в трех функциях: split, merge и mergesort. Также обратите внимание на отсутствие типов, за исключением синтаксиса и , которые обозначают списки. Этот код сортирует списки любого типа, если определена последовательная функция упорядочивания. Используя вывод типов Хиндли–Милнера , можно вывести типы всех переменных, даже сложные типы, такие как у функции .op ::[]cmpcmp
Расколоть
fun splitреализовано с помощью замыкания с сохранением состояния , которое переключается между trueи false, игнорируя входные данные:
fun alternator {} = let val state = ref true in fn a => !state before state := not ( !state ) end(* Разделить список на почти равные половины, которые будут либо одинаковой длины, * либо первая будет иметь на один элемент больше, чем другая. * Выполняется за время O(n), где n = |xs|. *) fun split xs = List . partition ( alternator {}) xsСлияние
Merge использует локальный цикл функций для эффективности. Внутренний loopопределяется в терминах случаев: когда оба списка непустые ( ) и когда один список пуст ( ).x :: xs[]
Эта функция объединяет два отсортированных списка в один отсортированный список. Обратите внимание, как аккумулятор accстроится в обратном порядке, а затем переворачивается перед возвратом. Это распространенная техника, поскольку представлена в виде связанного списка ; эта техника требует больше времени, но асимптотика не хуже.'a list
(* Объединить два упорядоченных списка, используя order cmp. * Pre: каждый список должен быть уже упорядочен по cmp. * Выполняется за время O(n), где 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Сортировка слиянием
Основная функция:
весело ap f ( x , y ) = ( f x , f y )(* Сортирует список в соответствии с заданной операцией упорядочения cmp. * Выполняется за время O(n log n), где n = |xs|. *) fun mergesort cmp [] = [] | mergesort cmp [ x ] = [ x ] | mergesort cmp xs = ( merge cmp o ap ( mergesort cmp ) o split ) xsБыструю сортировку можно выразить следующим образом. — это замыкание , которое потребляет оператор порядка .fun partop <<
инфикс <<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Обратите внимание на относительную легкость, с которой можно определить и обработать небольшой язык выражений:
исключение TyErr ;тип данных ty = IntTy | BoolTyзабавно объединить ( IntTy , IntTy ) = IntTy | объединить ( BoolTy , BoolTy ) = BoolTy | объединить (_, _) = raise TyErr тип данных exp = True | False | Int из int | Не из exp | Добавить exp * exp | Если 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 )) и assert e t = unify ( infer e , t )забавный 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 )) (* правильно типизировано *) val NONE = run ( If ( Not ( Int 1 ), True , False )) (* неправильно типизировано *)Модуль IntInfобеспечивает целочисленную арифметику произвольной точности. Более того, целочисленные литералы могут использоваться как целые числа произвольной точности без необходимости каких-либо действий со стороны программиста.
Следующая программа реализует факториальную функцию произвольной точности:
Каррированные функции имеют множество применений, например, устранение избыточного кода. Например, модуль может требовать функции типа , но удобнее писать функции типа , где есть фиксированная связь между объектами типа и . Функция типа может вынести эту общность за скобки. Это пример шаблона адаптера . [ необходима цитата ]a -> ba * c -> bacc -> (a * c -> b) -> a -> b
В этом примере вычисляется численная производная заданной функции в точке :fun dfx
- fun d delta f x = ( f ( x + delta ) - f ( x - delta )) / ( 2.0 * delta ) val d = fn : вещественное -> ( вещественное -> вещественное ) -> вещественное -> вещественноеТип указывает, что он отображает «float» на функцию с типом . Это позволяет нам частично применять аргументы, что известно как каррирование . В этом случае функция может быть специализирована путем частичного применения ее с аргументом . Хорошим выбором для при использовании этого алгоритма является кубический корень машинного эпсилон . [ необходима цитата ]fun d(real -> real) -> real -> realddeltadelta
- val d' = d 1E~8 ; val d' = fn : ( действительный -> действительный ) -> действительный -> действительныйВыведенный тип указывает, что d'ожидает функцию с типом в качестве первого аргумента. Мы можем вычислить приближение к производной от . Правильный ответ — .real -> real
- d' ( fn x => x * x * x - x - 1.0 ) 3.0 ; значение it = 25.9999996644 : реальноеБиблиотека Basis [7] была стандартизирована и поставляется с большинством реализаций. Она предоставляет модули для деревьев, массивов и других структур данных, а также интерфейсы ввода/вывода и системные интерфейсы.
Для численных вычислений существует модуль Matrix (но в настоящее время он не работает), https://www.cs.cmu.edu/afs/cs/project/pscico/pscico/src/matrix/README.html.
Для графики cairo-sml — это интерфейс с открытым исходным кодом для графической библиотеки Cairo . Для машинного обучения существует библиотека для графических моделей.
Реализации стандартного ML включают в себя следующее:
Стандарт
Производный
Исследовать
Все эти реализации имеют открытый исходный код и находятся в свободном доступе. Большинство из них реализованы в Standard ML. Коммерческих реализаций больше нет; Harlequin , ныне несуществующая, когда-то выпустила коммерческую IDE и компилятор под названием MLWorks, которая перешла к Xanalys и позже стала открытой после того, как была приобретена Ravenbrook Limited 26 апреля 2013 года.
Вся корпоративная архитектура ИТ- университета Копенгагена реализована примерно в 100 000 строк SML, включая записи о персонале, расчет заработной платы, администрирование курсов и обратную связь, управление студенческими проектами и веб-интерфейсы самообслуживания. [8]
Помощники доказательства HOL4 , Isabelle , LEGO и Twelf написаны на стандартном ML. Он также используется разработчиками компиляторов и проектировщиками интегральных схем, такими как ARM . [9]
О стандартном ML
О преемнике ML
Практический
Академический