Почему ML называется Meta-Language?

Question

Как ML (и его варианты, например, SML) метаязык.Какой объектный язык описывает ML?Это просто потому, что функции считаются значениями, поэтому код обрабатывается так же, как данные?

Answer 1

На самом деле это исходный вариант использования.

ML был разработан как язык для написания доказательств теорем.В этом случае ML - это язык программирования, который вы используете для описания теории.Это язык выше теории: метаязык.Или, как сказал бы Милнер, в оригинальной статье :

Мы также обсуждаем распространение этих результатов на более богатые языки;алгоритм проверки типа, основанный на W, фактически уже реализован и работает для метаязыка ML в системе LCF в Эдинбурге.

Имя застряло, поэтому теперь оно называется так, хотя и нене описывать объектный язык в общем смысле.

Answer 2

ML изначально был мета-языком для теоремы LCF, разработанной Милнером в 70-х годах.Вы можете использовать его для определения и выполнения доказательств в этой системе, например, путем написания тактики доказательств в ML.Смотрите также статья в Википедии