Прежде всего, давайте начнем с короткого экскурса в историю OCaml . Ксавье Леруа не изобрел язык, и ни один язык не родился во Франции. OCaml родился от метаязыка (ML) теоремы LCF (Logi c для вычислимых функций), разработанного в Стэнфорде и Эдинбургском университете Робин Милнер . Ниже приведен фрагмент кода, полученный из оригинального LCF 1977 года,
let gensrinfo th =
let srthm = disjsrvars th in
let hypfrees = formlfrees(hyp srthm)
and hyptyvars = formltyvars(hyp srthm)
and (),p,() = destimpequiv(concl srthm) in
srthm , termmatch(hypfrees,hyptyvars) p;;
Это напоминает что-то? ;) Это было немного позже, когда французская команда Formel разработала новую реализацию ML, основанную на категориальной абстрактной машине, которая позже превратилась в SML, и сам Caml родился на 10 лет позже, чем код. фрагмент приведен выше в 1987 году. А три года спустя, в 1990 году, Ксавье Леруа разработал совершенно новую реализацию Caml на основе интерпретатора байт-кода под названием ZIN C. Пять лет спустя они разработали оптимизирующий компилятор, и еще пять лет спустя, в 2000 году, родился Objective Caml, он же O'Caml, а теперь и OCaml.
Это все, что изначально означало ML был разработан и разработан сообществом говорящих на английском языке Engli sh, и нет никаких оснований искать этимологию конвенции на французском языке или предпочтения Ксавье. Мы действительно можем найти это соглашение уже в LCF (например, intoftok
, tokofint
операторы) и в других производных LCF, таких как HOL, например, стандартная библиотека HOL 1988 уже имела функцию int_of_string , в то время Ксавье еще даже не закончил.
Итак, почему это соглашение? Это происходит из рассуждений о программах, которые логичны, а не обязательны (помните, что ML родился как мета-язык (язык logi c) в программе проверки теорем). Вместо того, чтобы думать о , как реализована функция, мы думаем о , что представляет термин, и что такое int_of_string "42"
? Это целое число, которое имеет текстовое представление «42». Мы не конвертируем"42" в целое число и думаем о нем как о поле преобразования, вместо этого мы используем декларативное мышление, как в математике, например, cos 0.0
не конвертирует 0.0
в 1.0
, cos 0.0
равно 1.0
. Этот стиль мышления облегчает эквациональное мышление - мощный способ мышления о программах и понимания их семантики.