ML

ML (Meta Language) — сімейство строго типізованих мов функціонального програмування з розвиненою поліморфною системою типів і модулями, що параметризуються. Подібна система типів була раніше запропонована Роджером Гіндлі у 1969 році і зараз^[коли?] часто називається системою Гіндлі-Мілнера. Мови даного сімейства не є чистими функціональними мовами, тому що включають і імперативні інструкції. ML викладається у багатьох західних університетах (в деяких навіть як перша мова програмування).

Передумови[ред. | ред. код]

В 1963 у Джон Алан Робінсон реалізував метод автоматичного доведення теорем, що отримав назву «принцип резолюції». Ідея цього методу належить Жаку Ербрану, і запропонована у 1930. Робінсон розробив ефективний з обчислювальної точки зору алгоритм уніфікації, що є основою методу. Так з'явилася мова ML, створена для автоматичного доведення теорем, але як виявилося придатна і як мова програмування загального призначення.

Особливості[ред. | ред. код]

В основі строгої і статичної системи типів мови лежить лямбда-числення, до якого додана строга типізація. Строга система типів робить можливості для оптимізації, тому незабаром з'являється компілятор мови. В системі типів Гіндлі-Мілнера обмежено поліморфна система типів, де більшість типів виразів може бути виведено автоматично. Це дає можливість програмісту не описувати явно типи функцій, але зберегти строгий контроль типів.

Приклад[ред. | ред. код]

Обчислення факторіалу на ML:

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

Див. також[ред. | ред. код]

• Система F

Посилання[ред. | ред. код]

• Стаття ML [Архівовано 10 травня 2013 у Wayback Machine.] у Прогопедії — енциклопедії мов програмування(рос.)
• https://web.archive.org/web/20120718184406/http://schools.keldysh.ru/sch444/museum/LANR/ml.htm

Це незавершена стаття про мови програмування. Ви можете допомогти проєкту, виправивши або дописавши її.