Loading AI tools
ML (Meta Language) — семейство строгих языков функционального программирования с развитой параметрически полиморфной системой типов и параметризуемыми модулями. Подобная система типов была раньше предложена Роджером Хиндли в 1969 году и сейчас часто называется системой Хиндли-Милнера. Языки данного семейства в большинстве своём не являются чистыми функциональными языками, так как включают и императивные инструкции (но есть исключения — например, Manticore). ML преподаётся во многих западных университетах (в некоторых даже как первый язык программирования).
| ML | |
|---|---|
| Семантика | мультипарадигменный: функциональный, императивный, модульный |
| Класс языка | язык программирования, процедурный язык программирования и язык функционального программирования |
| Появился в | 1973 |
| Автор | Робин Милнер и др. - Эдинбургский университет |
| Система типов | сильная, статическая, выводная |
| Диалекты | Standard ML, Caml Light, OCaml, F#[1], LazyML |
| Испытал влияние | ISWIM |
| Повлиял на | Miranda, Haskell, Cyclone, Nemerle, C++ |
В 1963 году Джон Алан Робинсон реализовал метод автоматического доказательства теорем, получивший название «принцип резолюции». Идея этого метода принадлежит Эрбрану; она была предложена в 1930 году. Робинсон разработал эффективный с вычислительной точки зрения алгоритм унификации, являющийся основой метода.
В 1969 году Дана Скотт распространил меморандум, официально не опубликованный до 1993 года[2]. В меморандуме была предложена дедуктивная система 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).
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
