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

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

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

Язык [ править ]

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

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

 забавный  факториал  n  =  если  n  =  0,  то  1  иначе  n  *  факториал  ( n  -  1 )

Компилятор Standard ML необходим для определения статического типа int -> intэтой функции без аннотаций типов, предоставляемых пользователем. Т.е. он должен сделать вывод, что n используется только с целочисленными выражениями и, следовательно, само должно быть целым числом, и что все выражения, производящие значение, в функции возвращают целые числа.

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

 забавный  факториал  0  =  1  |  факториал  n  =  n  *  факториал  ( n  -  1 )

Это можно переписать, используя оператор case следующим образом:

 val  rec  factorial  =  fn  n  =>  случай  n  из  0  =>  1  |  n  =>  n  *  факториал  ( n  -  1 )

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

fun  factorialIT  value  = let  val  flag  =  ref  value  и  i  =  ref  1 in  while  ! flag  <>  0  do  (  i  : =  ! i  *  ! flag ;  flag  : =  ! flag  -  1  );  ! я конец ;

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

 val  rec  factorial  =  fn  0  =>  1  |  n  =>  n  *  факториал ( n  -  1 )

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

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

 забавный  факториал  n  =  let  fun  lp  ( 0 ,  acc )  =  acc  |  lp  ( m ,  acc )  =  lp  ( m- 1 ,  m * acc )  in  lp  ( n ,  1 )  конец

(Значение let -expression - это значение выражения между in и end .) Инкапсуляция сохраняющего инвариант хвостового рекурсивного жесткого цикла с одним или несколькими параметрами аккумулятора внутри внешней функции без инвариантов, как показано здесь, является распространенная идиома в стандартном машинном обучении и очень часто появляется в коде SML.

Введите синонимы [ править ]

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

 тип  loc  =  real  *  real fun  dist  (( x0 ,  y0 ),  ( x1 ,  y1 ))  =  let  val  dx  =  x1  -  x0  val  dy  =  y1  -  y0  в  математике . sqrt  ( dx  *  dx  +  dy  *  dy )  конец весело  цапля  ( a ,  b ,  c )  =  let  val  ab  =  dist  ( a ,  b )  val  bc  =  dist  ( b ,  c )  val  ac  =  dist  ( a ,  c )  val  perim  =  ab  +  bc  +  ac  val  s  =  perim  /  2.0  в  математике . sqrt  (s  *  ( s  -  ab )  *  ( s  -  bc )  *  ( s  -  ac ))  конец

Алгебраические типы данных и сопоставление с образцом [ править ]

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

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

Тип данных  форма  =  круг  из  LOC  *  реальный  (* центр и радиус *)  |  Площадь  от  LOC  *  реальная  (* верхний левый угол и длина боковой; ось выровненных *)  |  Треугольник  из  LOC  *  LOC  *  LOC  (* углы *)

(См. Определение выше loc.) Примечание: для определения рекурсивных конструкторов необходимы типы данных, а не синонимы типов. (В данном примере это не проблема.)

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

забавная  зона  ( Круг  (_,  r ))  =  3,14  *  r  *  r  |  площадь  ( Квадрат  (_,  s ))  =  s  *  s  |  площадь  ( Треугольник  ( a ,  b ,  c ))  =  цапля  ( a ,  b ,  c )  (* см. выше *)

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

Определение функции в стиле так называемой "клаузальной формы", в которой шаблоны появляются сразу после имени функции, является просто синтаксическим сахаром для

весело  площадь  форма  =  случае  форма  из  круга  (_,  г )  =>  3,14  *  г  *  г  |  Квадрат  (_,  s )  =>  s  *  s  |  Треугольник  ( a ,  b ,  c )  =>  цапля  ( a ,  b ,  c )

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

 центр  развлечений ( Круг  ( c ,  _))  =  c  |  центр  ( Квадрат  (( x ,  y ),  s ))  =  ( x  +  s  /  2,0 ,  y  +  s  /  2,0 )

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

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

весело  hasCorners  ( Circle  _)  =  false  |  hasCorners  _  =  истина

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

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

весело  f  ( Круг  (( x ,  y ),  r ))  =  x + y  |  f  ( Круг  _)  =  1.0  |  f  _  =  0,0

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

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

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

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

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

 весело  applyToBoth  f  x  y  =  ( f  x ,  f  y )

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

 fun  constant  Fn k  =  let  fun  const  something  =  k  in  const  end

(альтернативно)

  константа  веселья Fn k  =  ( fn  something  =>  k )

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

 fun  compose  ( f ,  g )  =  let  fun  h  x  =  f  ( g  x )  в  конце h 

(альтернативно)

 весело  сочинять  ( f ,  g )  =  ( fn  x  =>  f  ( g  x ))

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

 забавная  карта  _  []  =  []  |  карта  f  ( x :: xs )  =  f  x  ::  map  f  xs

(Более эффективная реализация mapбудет определять хвостовой рекурсивный внутренний цикл следующим образом :)

 забавная  карта  f  xs  =  let  fun  m  ([],  acc )  =  List . rev  acc  |  m  ( x :: xs ,  acc )  =  m  ( xs ,  f  x  ::  acc )  in  m  ( xs ,  [])  конец

Исключения [ править ]

Исключения вызываются raiseключевым словом и обрабатываются handleконструкциями сопоставления с образцом .

 исключение  Неопределенное  веселье  max  [ x ]  =  x  |  max  ( x :: xs )  =  let  val  m  =  max  xs  in  if  x  >  m  then  x  else  m  end  |  max  []  =  поднять  Undefined  fun  main  xs  =  let  val  msg  =  ( Int . toString  ( max  xs ))  дескриптор Undefined  =>  "пустой список ... нет максимума!"  в  печати  ( msg  ^  " \ n " )  конец

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

 исключение  Zero  fun  listProd  ns  =  let  fun  p  []  =  1  |  p  ( 0 :: _)  =  поднять  ноль  |  p  ( h :: t )  =  h  *  p  t  in  ( p  ns )  handle  Ноль  =>  0  конец

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

Модульная система [ править ]

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

Систему модулей SML составляют три основные синтаксические конструкции: структуры, сигнатуры и функторы. Структура представляет собой модуль; он состоит из набора типов, исключений, значений и структур (называемых подструктурами ), упакованных вместе в логическую единицу. Подпись является интерфейс , обычно мыслится как тип для структуры: она указывает имена всех лиц , предусмотренных структурой, а также арностей компонентов типа, типы компонентов ценности и подписи для подструктур. Определения компонентов типа могут или не могут быть экспортированы; Компоненты типа, определения которых скрыты, являются абстрактными типами . Наконец, функторэто функция от структур к структурам; то есть функтор принимает один или несколько аргументов, которые обычно являются структурами данной сигнатуры, и создает структуру в качестве своего результата. Функторы используются для реализации общих структур данных и алгоритмов.

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

 подпись  QUEUE  =  sig  type  '  исключение очереди  QueueError val empty : ' a queue val isEmpty : 'a queue -> bool val singleton : ' a -> 'a queue val insert : ' a * 'a queue -> ' a queue val peek : ' очередь -> ' a val remove : ' очередь -> ' a                                             *  '  конец очереди 

Эта сигнатура описывает модуль, который предоставляет параметризованный тип queueочередей, вызываемое исключение QueueErrorи шесть значений (пять из которых являются функциями), обеспечивающими основные операции с очередями. Теперь можно реализовать структуру данных очереди, написав структуру с этой подписью:

 структура  TwoListQueue  :>  QUEUE  =  тип структуры  'a queue = ' список * ' исключение списка QueueError            val  empty  =  ([], [])  fun  isEmpty  ([], [])  =  true  |  isEmpty  _  =  false  забавный  синглтон  a  =  ([],  [ a ])  забавная  вставка  ( a ,  ([],  []))  =  ([],  [ a ])  |  вставить  ( а ,  ( входы ,  выходы ))  =  ( а :: входы ,  выходы )  fun  peek  (_, [])  =  поднять  QueueError  |  peek  ( ins ,  a :: out )  =  a  весело  удалить  (_, [])  =  поднять  QueueError  |  remove  ( ins ,  [ a ])  =  ( a ,  ([],  rev  ins ))  |  remove  ( ins ,  a :: out )  =  ( a ,  ( ins , out ))  конец

Это определение заявляет, что TwoListQueueэто реализация QUEUEподписи. Кроме того, непрозрачное приписывание (обозначается :>) утверждает, что любые компоненты типа, определения которых не указаны в сигнатуре ( т. Е. queue ), Должны рассматриваться как абстрактные, что означает, что определение очереди как пары списков не видно за пределами модуля. . Тело структуры обеспечивает привязки для всех компонентов, перечисленных в подписи.

Чтобы использовать структуру, можно получить доступ к ее элементам типа и значения, используя "точечную нотацию". Например, очередь строк будет иметь тип string TwoListQueue.queue, пустая очередь TwoListQueue.empty, и чтобы удалить первый элемент из очереди, нужно qнаписать TwoListQueue.remove q.

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

 функтор  BFS  ( структура  Q :  QUEUE )  =  (* после Okasaki, ICFP, 2000 *)  struct  datatype  'a  tree  =  E  |  Т  о  «а  *  » а  дерево  *  «а  дерево  весело  bfsQ  ( д  :  » а  дерево  Q . Очередь )  :  «а  список  =  если  Q . isEmpty  q  then  []  иначе  пусть  val  ( t,  Д» )  =  Q . удалить  q  в  случае  t  из  E  =>  bfsQ  q '  |  Т  ( х ,  л ,  г )  =>  пусть  вал  Q ''  =  Q . вставки  ( г ,  Q . вставка  ( л ,  д» ))  в  х  ::  bfsQ  Q ''  Конец  конца  потехи  BFS  т  =  bfsQ  (Вопрос . singleton  t )  конец

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

Библиотеки [ править ]

Стандарт [ править ]

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

Третья сторона [ править ]

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

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

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

Примеры кода [ править ]

Фрагменты кода SML легче всего изучать, вводя их в «верхний уровень», также известный как цикл чтения-оценки-печати или REPL. Это интерактивный сеанс, который распечатывает предполагаемые типы результирующих или определенных выражений. Многие реализации SML предоставляют интерактивный REPL, включая SML / NJ :

$ sml Standard ML of New Jersey v110.52 [построено: 21 января, пт, 16:42:10 2005] -

Затем можно ввести код в ответ на приглашение «-». Например, чтобы вычислить 1 + 2 * 3:

 -  1  +  2  *  3 ;  val  it  =  7  :  int

Верхний уровень определяет тип выражения как «int» и возвращает результат «7».

Привет, мир [ править ]

Следующая программа "hello.sml":

 print  "Привет, мир! \ n " ;

может быть скомпилирован с помощью MLton:

$ mlton hello.sml

и выполнено:

$ ./hello Привет мир!

Вставка сортировки [ править ]

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

 fun  ins  ( n ,  [])  =  [ n ]  |  ins  ( n ,  ns  as  h :: t )  =  if  ( n <h )  then  n :: ns  else  h :: ( ins  ( n ,  t ))  val  insertSort  =  List . foldr  ins  []

Это можно сделать полиморфным, абстрагируясь от оператора упорядочивания. Здесь мы используем символическое имя <<для этого оператора.

 fun  ins '  <<  ( num ,  nums )  =  let  fun  i  ( n ,  [])  =  [ n ]  |  i  ( n ,  ns  as  h :: t )  =  if  << ( n , h )  then  n :: ns  else  h :: i ( n , t )  in  i  ( num ,  nums )  end  fun  insertSort '  << =  Список . foldr  ( ins '  << )  []

Тип insertionSort'есть ('a * 'a -> bool) -> ('a list) -> ('a list).

Пример вызова:

-  InsertSort '  op <  [ 3 ,  1 ,  4 ]; val  it  =  [ 1 , 3 , 4 ]  :  список int 

Сортировка слияния [ править ]

Здесь классический алгоритм сортировки слиянием реализован в трех функциях: разделение, слияние и сортировка слиянием.

Функция splitреализована с помощью локальной функции с именем loop, у которой есть два дополнительных параметра. Локальная функция loopнаписана в стиле хвостовой рекурсии ; как таковой его можно эффективно компилировать. Эта функция использует синтаксис сопоставления с образцом SML, чтобы различать случаи непустого списка ( x::xs) и пустого списка ( []). Для стабильности список ввода nsперед передачей ему переворачивается loop.

 (* Разделить список на две почти половинки, возвращается как пара.  * «Половинки» будут либо одного размера,  * или первая будет иметь на один элемент больше, чем вторая.  * Выполняется за O (n) раз, где n = | xs |. *)  цикл локального  развлечения  ( x :: y :: zs , xs , ys ) = цикл ( zs , x :: xs , y :: ys ) | цикл ( x :: [], xs , ys ) = ( x :: xs , ys ) | цикл ([], xs ,                     ys )  =  ( xs ,  ys )  в  fun  split  ns  =  loop  ( List . rev  ns ,  [],  [])  end

Синтаксис local-in-end можно заменить синтаксисом let-in-end, что даст эквивалентное определение:

 fun  split  ns  =  let  fun  loop  ( x :: y :: zs ,  xs ,  ys )  =  loop  ( zs ,  x :: xs ,  y :: ys )  |  цикл  ( x :: [],  xs ,  ys )  =  ( x :: xs ,  ys )  |  loop  ([],  xs ,  ys )  =  ( xs ,  ys )  в  цикле  ( List .rev  ns ,  [],  [])  конец

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

Эта функция объединяет два «восходящих» списка в один восходящий список. Обратите внимание на то, как аккумулятор outстроится «в обратном направлении», а затем переворачивается List.revперед возвратом. Это распространенный метод - построить список в обратном порядке, а затем перевернуть его перед возвратом. В SML списки представлены в виде связанного списка элементов , поэтому эффективно добавлять элемент к списку, но неэффективно добавлять элемент в список. Дополнительный проход по списку - это операция с линейным временем , поэтому, хотя этот метод требует большего времени на настенных часах, асимптотика не хуже.

 (* Объедините два упорядоченных списка, используя порядок lt.  * Pre: указанные списки xs и ys уже должны быть упорядочены на lt.  * Выполняется за время O (n), где n = | xs | + | ys |. *)  Fun  merge  lt  ( xs ,  ys )  =  let  fun  loop  ( out ,  left  as  x :: xs ,  right  as  y :: ys )  =  if  lt  ( x ,  y )  then  loop  ( x :: out ,  xs ,  right )  else  loop  (y :: out ,  left ,  ys )  |  loop  ( out ,  x :: xs ,  [])  =  loop  ( x :: out ,  xs ,  [])  |  loop  ( out ,  [],  y :: ys )  =  loop  ( y :: out ,  [],  ys )  |  loop  ( out ,  [],  [])  =  Список . изм  из  в  петле  ([],  хз , ys )  конец

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

 (* Сортировать список в соответствии с заданной операцией упорядочения lt.  * Выполняется за O (n log n) раз, где n = | xs |.  *)  Fun  mergesort  lt  xs  =  let  val  merge '  =  merge  lt  fun  ms  []  =  []  |  ms  [ x ]  =  [ x ]  |  ms  xs  =  let  val  ( left ,  right )  =  split  xs  in  merge '  ( ms  left ,  ms справа )  конец  через  мс  хз  конец

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

Быстрая сортировка [ править ]

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

 fun  quicksort  <<  xs  =  let  fun  qs  []  =  []  |  qs  [ x ]  =  [ x ]  |  qs  ( p :: xs )  =  let  val  ( меньше ,  больше )  =  Список . partition  ( fn  x  =>  <<  ( x ,  p ))  xs  в  qs  меньше  @  p  ::  qs  больше конец  в  qs  xs  конец

Написание языкового переводчика [ править ]

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

 исключение  Err  тип данных  ty  =  IntTy  |  BoolTy  тип данных  exp  =  True  |  Ложь  |  Int  из  int  |  Не  из  ехр  |  Добавить  в  ехр  *  ехр  |  Если  в  ехр  *  ехр  *  ехр  fun  typeOf  ( True )  =  BoolTy  |  typeOf  ( False )  =  BoolTy  |  typeOf  ( Int  _)  =  IntTy  |  TYPEOF  ( не  е )  =  если  TYPEOF  е  =  BoolTy  то  BoolTy  еще  рейз  Err  |  typeOf  ( Добавить  ( e1 ,  e2 ))  =  if  ( typeOf  e1  =  IntTy)  Атакже  ( TYPEOF  e2  =  IntTy ) ,  то  IntTy  еще  рейз  Err  |  typeOf  ( If  ( e1 ,  e2 ,  e3 ))  =  if  typeOf  e1  <>  BoolTy  затем  поднять  Err  else  if  typeOf  e2  <>  typeOf  e3  затем  поднять  Err  else  typeOf  e2  весело  eval  ( True )  =  True  |  eval  ( False )  =  False  |  eval  ( Int  n )  =  Int  n  |  eval  ( Not  e )  =  ( case  eval  e  of  True  =>  False  |  False  =>  True  |  _  =>  raise  Fail  "проверка типов не работает" )  |  eval  ( Добавить  (e1 ,  e2 ))  =  let  val  ( Int  n1 )  =  eval  e1  val  ( Int  n2 )  =  eval  e2  в  Int  ( n1  +  n2 )  end  |  eval  ( If  ( e1 ,  e2 ,  e3 ))  =  если  eval  e1  =  True,  то  eval  e2  иначе  eval  e3  fun  chkEval  e  =  ( ignore  ( typeOf  e );  eval  e )  (* вызовет Err при ошибке типа *)

Пример использования на правильно напечатанных и неправильно набранных примерах:

-  val  e1  =  Add ( Int ( 1 ),  Int ( 2 ));  (* Правильно набрано *) val  e1  =  Add  ( Int  1 , Int  2 )  :  exp -  chkEval  e1 ; val  it  =  Int  3  :  exp-  val  e2  =  Add ( Int ( 1 ), True );  (* Неверно набрано *) val  e2  =  Add  ( Int  1 , True )  :  exp -  chkEval  e2 ; неперехваченное  исключение  Err

Факториальная функция произвольной точности (библиотеки) [ править ]

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

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

 весело  факт  п  :  IntInf . int  =  если  n = 0,  то  1  иначе  n  *  факт ( n  -  1 ) val  ()  =  print  ( IntInf . toString  ( факт  120 )  ^  " \ n " )

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

$ Mlton fact.sml $ ./fact 66895029134491270575881180540903725867527463331380298102956713523016335 57244962989366874165271984981308157637893214090552534408589408121859898 481114389650005964960521256960000000000000000000000000000

Числовая производная (функции высшего порядка) [ править ]

Поскольку SML - это функциональный язык программирования, в программах SML легко создавать и передавать функции. Эта возможность имеет огромное количество приложений. Вычисление числовой производной функции - одно из таких приложений. Следующая функция SML "d" вычисляет числовую производную заданной функции "f" в заданной точке "x":

 -  fun  d  delta  f  x  =  ( f  ( x  +  delta )  -  f  ( x  -  delta ))  /  ( 2,0  *  дельта );  val  d  =  fn  :  real  ->  ( real  ->  real )  ->  real  ->  real

Эта функция требует небольшого значения «дельта». Хорошим выбором для дельты при использовании этого алгоритма является кубический корень машинного эпсилона . ^{[ необходима цитата ]}

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

 -  val  d  =  d  1E ~ 8 ;  val  d  =  fn  :  ( реальный  ->  реальный )  ->  реальный  ->  реальный

Обратите внимание, что предполагаемый тип указывает, что замена «d» ожидает функцию с типом «real -> real» в качестве первого аргумента. Мы можем вычислить численное приближение к производной at с помощью:${\ Displaystyle е (х) = х ^ {3} -x-1}$${\ displaystyle x = 3}$

 -  d  ( fn  x  =>  x  *  x  *  x  -  x  -  1,0 )  3,0 ;  val  it  =  25.9999996644  :  реальный

Правильный ответ ; .${\ displaystyle f '(x) = 3x ^ {2} -1}$${\ displaystyle f '(3) = 27-1 = 26}$

Функция «d» называется «функцией высшего порядка», потому что она принимает другую функцию («f») в качестве аргумента.

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

Дискретное вейвлет-преобразование (сопоставление с образцом) [ править ]

1D Хаара вейвлет - преобразования из целого числа -степени-из-двух длин список номеров могут быть реализованы очень кратко в SML и является отличным примером использования сопоставления с образцом по спискам, беря пар элементов ( «h1» и " h2 ") и сохраняя их суммы и разности в списках" s "и" d "соответственно:

 -  весело  haar  l  =  let  fun  aux  [ s ]  []  d  =  s  ::  d  |  вспомогательный  []  s  d  =  вспомогательный  s  []  d  |  aux  ( h1 :: h2 :: t )  s  d  =  aux  t  ( h1 + h2  ::  s )  ( h1-h2  ::  d )  |  aux  _  _  _  =  поднять  пустой  на  доп. l  []  []  конец ;  val  haar  =  fn  :  список целых  -> список целых   

Например:

 -  хаар  [ 1 ,  2 ,  3 ,  4 ,  ~ 4 ,  ~ 3 ,  ~ 2 ,  ~ 1 ];  val  it  =  [ 0 , 20 , 4 , 4 , ~ 1 , ~ 1 , ~ 1 , ~ 1 ]  :  int  list

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

Реализации [ править ]

Существует множество реализаций SML, в том числе:

• Стандартный ML Нью-Джерси (сокращенно SML / NJ) - это полный компилятор со связанными библиотеками, инструментами, интерактивной оболочкой и документацией. [1]
• Moscow ML - это облегченная реализация, основанная на среде исполнения CAML Light . Он реализует полный язык SML, включая модули SML и большую часть базовой библиотеки SML. [2]
• MLton - это компилятор, оптимизирующий всю программу, который производит очень быстрый код по сравнению с другими реализациями ML. [3]
• ML Kit объединяет сборщик мусора (который может быть отключен) и регионом на основе управление памятью с автоматическим выводом областей, с целью поддержки приложений реального времени. Его реализация очень близко основана на Определении.
• Poly / ML - это полная реализация Standard ML, которая создает быстрый код и поддерживает многоядерное оборудование (через потоки Posix); его система времени выполнения выполняет параллельную сборку мусора и онлайн-совместное использование неизменяемых подструктур.
• Isabelle / ML интегрирует параллельный Poly / ML в интерактивное средство доказательства теорем со сложной IDE (на основе jEdit ) для официального стандартного ML (SML'97), диалектом Isabelle / ML и языком доказательства. Начиная с Isabelle2016, есть также отладчик исходного кода для ML.
• CakeML ^[6] версия ML цикла чтения-оценки-печати с формально проверенной средой выполнения и переводом на ассемблер.
• HaMLet - это интерпретатор SML, цель которого - быть точной и доступной эталонной реализацией стандарта.
• TILT - это полностью сертифицирующий компилятор для SML. Он использует типизированные промежуточные языки для оптимизации кода и обеспечения правильности и может компилироваться на типизированный язык ассемблера .
• SML.NET позволяет компилировать в Microsoft CLR и имеет расширения для связывания с другим кодом .NET .
• SML2c - это пакетный компилятор, который компилирует в C только объявления на уровне модуля (т.е. сигнатуры, структуры, функторы) . Он основан на SML / NJ версии 0.67 и имеет общий интерфейс и большую часть своей системы времени выполнения, но не поддерживает отладку и профилирование в стиле SML / NJ. Программы уровня модуля, которые работают на SML / NJ, могут быть скомпилированы sml2c без изменений.
• Система Poplog реализует версию SML с POP-11 и, возможно, Common Lisp и Prolog , что позволяет программировать на разных языках. Для всех языком реализации является POP-11, который компилируется постепенно. Он также имеет встроенный редактор, подобный Emacs, который взаимодействует с компилятором.
• SML # - это расширение SML, обеспечивающее полиморфизм записей и взаимодействие с языком C. Это обычный собственный компилятор, и его название не является намеком на работу на платформе .NET.
• Алиса : интерпретатор для Standard ML от Саарландского университета, добавляющий функции для отложенного вычисления , параллелизма ( многопоточность и распределенные вычисления через удаленные вызовы процедур ) и программирования ограничений .
• SOSML - это реализация SML, написанная на TypeScript, которая запускается непосредственно в веб-браузере. Он реализует большую часть языка SML и отдельные части базовой библиотеки SML.

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

Основные проекты, использующие SML [ править ]

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

Помощники доказательства HOL4 , Isabelle , LEGO и Twelf написаны на SML.

SML широко используется разработчиками компиляторов и микросхем, например, ARM . ^{[ необходима цитата ]}

См. Также [ править ]

• F #
• OCaml

Ссылки [ править ]

Внешние ссылки [ править ]

• Стандартный проект семейства ML на GitHub
• Стандартный язык машинного обучения Мадс Тофте, Scholarpedia , 4 (2): 7515. DOI: 10.4249 / scholarpedia.7515
• Что такое SML?
• Что такое SML '97?
• преемник ML (sML) призван обеспечить средство продолжения эволюции ML с использованием Standard ML в качестве отправной точки.
• Программирование в стандартном ML
• Программирование в Standard ML '97: интерактивное руководство
• Univ. Чикаго - учебник по SML (слайды)
• CSE341: Языки программирования , Дэн Гроссман, Вашингтонский университет. Также на Coursera и YouTube