| ML | |
|---|---|
| Парадигма | процедурне програмування, функційне програмування і імперативне програмування  |
| Дата появи | 1973 |
| Творці | Робін Мілнер та ін. -Единбурзький університет |
| Розробник | Робін Мілнер |
| Система типізації | строга,статична,вивід типів |
| Діалекти | Standard ML,Caml Light,OCaml,F#,LazyML,OcaMl |
| Під впливом від | ISWIMd |
| Вплинула на | Miranda,Haskell,Cyclone,Nemerle,C++,Elm |
ML (Meta Language) — сімейство строго типізованих мов функціонального програмування з розвиненоюполіморфною системою типів і модулями, що параметризуються. Подібна система типів була раніше запропонована Роджером Гіндлі у1969 році і зараз[коли?] часто називається системою Гіндлі-Мілнера. Мови даного сімейства не є чистими функціональними мовами, тому що включають і імперативні інструкції. ML викладається у багатьох західних університетах (в деяких навіть як першамова програмування).
В1963 уДжон Алан Робінсон реалізував метод автоматичного доведення теорем, що отримав назву«принцип резолюції». Ідея цього методу належитьЖаку Ербрану, і запропонована у1930. Робінсон розробив ефективний з обчислювальної точки зоруалгоритм уніфікації, що є основою методу. Так з'явилася мова ML, створена дляавтоматичного доведення теорем, але як виявилося придатна і як мова програмування загального призначення.
В основі строгої і статичної системи типів мови лежитьлямбда-числення, до якого доданастрога типізація. Строга система типів робить можливості для оптимізації, тому незабаром з'являєтьсякомпілятор мови. В системі типів Гіндлі-Мілнера обмежено поліморфна система типів, де більшість типів виразів може бутививедено автоматично. Це дає можливість програмісту не описувати явно типи функцій, але зберегти строгий контроль типів.
Обчисленняфакторіалу на ML:
fun fac(n) = if n = 0 then 1 else n * fac(n-1);
 | Це незавершена стаття промови програмування. Ви можетедопомогти проєкту,виправивши або дописавши її. |