ML (Meta Language) — семейство строгих языков функционального программирования с развитой параметрически полиморфной системой типов и параметризуемыми модулями. Подобная система типов была раньше предложена в 1969 году и сейчас часто называется системой Хиндли-Милнера . Языки данного семейства в большинстве своём не являются чистыми функциональными языками, так как включают и императивные инструкции (но есть исключения — например, Manticore ). ML преподаётся во многих западных университетах (в некоторых даже как первый язык программирования).

Предпосылки и история языка

В 1963 году Джон Алан Робинсон реализовал метод автоматического доказательства теорем, получивший название « принцип резолюции ». Идея этого метода принадлежит Эрбрану ; она была предложена в 1930 году . Робинсон разработал эффективный с вычислительной точки зрения , являющийся основой метода.

В 1969 году Дана Скотт распространил меморандум, официально не опубликованный до 1993 года . В меморандуме была предложена дедуктивная система Logic for Computable Functions (LCF) - "логика для вычислимых функций". Одноименную систему , предназначенную для автоматизации доказательства теорем, в начале 1970-х годов начали разрабатывать Робин Милнер и его сотрудники в Стэнфорде и Эдинбурге.

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

Особенности

В основе строгой и статической системы типов языка лежит лямбда-исчисление , к которому добавлена строгая типизация . Строгая система типов дает возможности для оптимизации, поэтому вскоре появляется компилятор языка. В системе типов Хиндли-Милнера ограниченно полиморфная система типов, где большинство типов выражений может быть выведено автоматически . Это даёт возможность программисту не описывать явно типы функций, но сохранить строгий контроль типов.

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

Примеры

Вычисление факториала на ML:

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

Хорошим примером, позволяющим оценить выразительную силу ML, служит реализация :

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

Для задачи поиска строки в словаре, сочетает молниеносную скорость префиксных деревьев с экономичностью двоичных в отношении памяти. Реализация на ML отличается компактностью и самодокументируемостью за счёт использования алгебраических типов , сопоставления с образцом , правила « последнее выражение в исполнимой цепочке является результатом всей функции » и возможности строить объекты агрегатных типов без предварительных объявлений. Также она отличается доказанной корректностью — в частности, исключением утечек памяти , характерных для Си / C++ ; или риска допущения ошибок в исходном коде, приводящих к зацикливанию программы с лавинообразным поглощением памяти, характерных для динамически типизируемых языков.

Система типов Хиндли — Милнера обеспечивает языкам высокий потенциал к оптимизации, так что снижение трудоёмкости и повышение стабильности программ является «бесплатным» (без потери эффективности), при условии наличия оптимизирующего компилятора (таких как OCaml или MLton ).

См. также

• Язык модулей ML
• Standard ML
• OCaml
• Haskell
• F#
• F*

Примечания

Ссылки

• в — энциклопедии языков программирования (рус.)
• — сравнение ряда языков семейства ML