Какова причина "let rec" для нечистого функционального языка OCaml?

Ответ 1

Когда вы определяете семантику определения функции, как разработчика языка, у вас есть выбор: либо сделать имя функции видимым в области своего собственного тела, либо нет. Оба варианта являются совершенно законными, например языки C-семейства, которые далеки от функциональности, все еще имеют имена определений, видимых в их сфере действия (это также распространяется на все определения на языке C, что делает этот int x = x + 1 законным). Язык OCaml решает дать нам дополнительную гибкость выбора самостоятельно. И это действительно здорово. Они решили сделать это невидимым по умолчанию, довольно спускное решение, так как большинство функций, которые мы пишем, не являются рекурсивными.

Что касается цитирования, это действительно не соответствует определениям функций - наиболее частому использованию ключевого слова rec. В основном это касается "Почему область определения функции не распространяется на тело модуля". Это совершенно другой вопрос. После некоторых исследований я нашел очень аналогичный вопрос, который имеет ответ, который может вас удовлетворить, цитата из него:

Итак, учитывая, что проверяющий тип должен знать, какие наборы определения взаимно рекурсивные, что он может сделать? Одна из возможностей просто провести анализ зависимостей во всех определениях в области, и переупорядочить их в наименьшие возможные группы. Хаскелл на самом деле делает это, но в таких языках, как F # (и OCaml и SML), которые имеют Неограниченные побочные эффекты, это плохая идея, потому что она может переупорядочить побочные эффекты тоже. Поэтому вместо этого он просит пользователя явно отмечать какие определения взаимно рекурсивные и, следовательно, должно происходить обобщение.

Даже без какого-либо переупорядочения с произвольными нечистыми выражениями, которые могут возникать в определении функции (побочный эффект определения, а не оценки), невозможно построить граф зависимостей. Рассмотрим дешифрование и выполнение функции из файла.

Подводя итог, мы имеем два варианта конструкции let rec, один - создать саморекурсивную функцию, например

 let rec seq acc = function
    | 0 -> acc
    | n -> seq (acc+1) (n-1)

Другим является определение взаимно-рекурсивных функций:

let rec odd n =
  if n = 0 then true
  else if n = 1 then false else even (n - 1)
and even n =
  if n = 0 then false
  else if n = 1 then true else odd (n - 1)

В первом случае нет технических причин придерживаться одного или другого решения. Это просто вопрос вкуса.

Второй случай сложнее. При выводе типа вам нужно разбить все определения функций на кластеры, состоящие из взаимозависимых определений, чтобы ограничить среду ввода. В OCaml это сложнее сделать, поскольку вам нужно учитывать побочные эффекты. (Или вы можете продолжить, не разбивая его на основные компоненты, но это приведет к другой проблеме - ваша система типов будет более ограничительной, то есть будет запрещена более допустимая программа).

Но, пересматривая исходный вопрос и цитату из RWO, я все еще уверен, что нет никаких технических причин для добавления флага rec. Рассмотрим, SML, который имеет те же проблемы, но по умолчанию включен rec. Существует техническая причина для синтаксиса let ... and ... для определения набора взаимно-рекурсивных функций. В SML этот синтаксис не требует, чтобы мы помещали флаг rec в OCaml, что давало нам большую гибкость, например способность менять значения с помощью выражения let x = y and y = x.

Ответ 2

Каковы технические причины, налагаемые на использование let rec, в то время как чистые функциональные языки не являются?

Рекурсивность - странный зверь. Это имеет отношение к чистоте, но оно немного более наклонное, чем это. Чтобы быть ясным, вы могли бы написать "alterna-Haskell", который сохраняет свою чистоту, свою лень, но по умолчанию не рекурсивно связан с let и требует какого-то маркера rec, как это делает OCaml. Некоторые даже предпочли бы это.

В сущности, существует только много разных вариантов "пусть". Если мы сравним let и let rec в OCaml, мы увидим небольшую разницу. В статической формальной семантике мы можем написать

Γ ⊢ E : A    Γ, x : A ⊢ F : B
-----------------------------
   Γ ⊢ let x = E in F : B

в котором говорится, что если мы можем доказать в переменной окружении Γ, что E имеет тип A, и если мы сможем доказать в той же переменной окружения Γ, дополненной x : A, что F : B, тогда мы может доказать, что в переменной среде Γ let x = E in F имеет тип B.

То, что нужно посмотреть, это аргумент Γ. Это всего лишь список ( "имя переменной", "значение" ), такие как [(x, 3); (y, "hello")] и увеличение списка, такого как Γ, x : A, просто означает consing (x, A) на него (извините, что синтаксис перевернулся).

В частности, напишем тот же формализм для let rec

Γ, x : A ⊢ E : A    Γ, x : A ⊢ F : B
-------------------------------------
       Γ ⊢ let rec x = E in F : B

В частности, единственное отличие состоит в том, что ни одно из наших помещений не работает в простой среде Γ; обе имеют право предположить существование переменной x.

В этом смысле let и let rec - просто разные звери.

Итак, что значит быть чистым? По самому строгому определению, из которого Haskell даже не участвует, мы должны устранить все эффекты, включая не прекращение. Единственный способ добиться этого - отвлечь нашу способность писать неограниченную рекурсию и тщательно ее заменять.

Существует множество языков без рекурсии. Возможно, самым важным является просто типизированное исчисление лямбда. В ней базовая форма - это регулярное лямбда-исчисление, но дополненная типизированной дисциплиной, где типы немного похожи на

type ty =
  | Base
  | Arr of ty * ty

Оказывается, что STLC не может представлять рекурсию --- Y combinator и всех других комбинаторов кузенов с фиксированной точкой не может быть введен. Таким образом, STLC не является Turing Complete.

Это бескомпромиссно чисто. Однако он достигает этой чистоты с самыми тупыми инструментами, однако, полностью запрещая рекурсию. Нам бы очень понравилась какая-то сбалансированная, тщательная рекурсия, которая не приведет к бесконфликтному - мы по-прежнему будем Тьюрингом Незавершенным, но не настолько искалеченным.

Некоторые языки используют эту игру. Есть умные способы добавления типизированной рекурсии назад по разделению между data и codata, который гарантирует, что вы не можете писать функции без прерывания. Если вам интересно, я предлагаю немного изучить Coq.

Но цель OCaml (и Haskell) не должна быть деликатной. Оба языка бескомпромиссны. Тьюринг завершен (и, следовательно, "практичен" ). Поэтому давайте обсудим еще несколько тупых способов увеличения STLC с рекурсией.

Самый грубый из них - добавить одну встроенную функцию fix

val fix : ('a -> 'a) -> 'a

или, в более оригинальной нотации OCaml-y, которая требует eta-расширения

val fix : (('a -> 'b) -> ('a -> 'b)) -> ('a -> 'b)

Теперь помните, что мы рассматриваем только примитивный STLC с fix. Мы действительно можем написать fix (последнее по крайней мере) в OCaml, но это мошенничество в данный момент. Что fix покупает STLC в качестве примитива?

Получается, что ответ: "все". STLC + Fix (в основном язык под названием PCF) нечист и Turing Complete. Это также просто чрезвычайно сложно использовать.

Итак, это окончательное препятствие для прыжка: как нам облегчить работу с fix? Добавляя рекурсивные привязки!

Уже, STLC имеет конструкцию let. Вы можете думать об этом как о синтаксисе сахара:

let x = E in F   ---->   (fun x -> F) (E)

но как только мы добавили fix, мы также можем ввести привязки let rec

let rec x a = E in F ----> (fun x -> F) (fix (fun x a -> E))

В этот момент снова должно быть ясно: let и let rec - очень разные звери. Они воплощают различные уровни лингвистической силы, а let rec - это окно, позволяющее фундаментальную примесь через полноту Тьюринга и ее отказ от партнерского эффекта.

Итак, в конце дня, немного забавно, что Haskell, более чистый из двух языков, сделал интересный выбор отмены простых привязок let. Это действительно единственное различие: синтаксиса для представления нерекурсивного связывания в Haskell нет.

На данный момент это по существу просто решение стиля. Авторы Haskell определили, что рекурсивные привязки были настолько полезны, что можно было также предположить, что каждое связывание является рекурсивным (и, во-вторых, может игнорировать червь в этом ответе).

С другой стороны, OCaml дает вам возможность полностью четко определять тип привязки, который вы выбираете, let или let rec!

Ответ 3

Я думаю, что это не имеет ничего общего с чисто функциональным, это просто дизайнерское решение, которое в Haskell вам не разрешено делать

let a = 0;;
let a = a + 1;;

тогда как вы можете сделать это в Caml.

В Haskell этот код не будет работать, потому что let a = a + 1 интерпретируется как рекурсивное определение и не прерывается. В Haskell вам не нужно указывать, что определение рекурсивно просто потому, что вы не можете создать нерекурсивный (поэтому ключевое слово rec есть везде, но не написано).

Ответ 4

Я не эксперт, но я сделаю предположение, пока появятся действительно знающие парни. В OCaml могут возникать побочные эффекты, возникающие при определении функции:

let rec f =
    let () = Printf.printf "hello\n" in
    fun x -> if x <= 0 then 12 else 1 + f (x - 1)

Это означает, что порядок определений функций должен быть сохранен в некотором смысле. Теперь представьте себе, что два разных набора взаимно-рекурсивных функций чередуются. Для компилятора совсем не легко сохранить порядок при обработке их как двух отдельных взаимно-рекурсивных наборов определений.

Использование `let rec... and`` означает, что различные группы взаимно-рекурсивных определений функций не могут чередоваться в OCaml, как они могут в Haskell. Haskell не имеет побочных эффектов (в некотором смысле), поэтому определения могут быть свободно переупорядочены.

Ответ 5

Это не вопрос чистоты, это вопрос определения среды, в которой typechecker должен проверять выражение. Это на самом деле дает вам больше силы, чем в противном случае. Например (я собираюсь написать Standard ML здесь, потому что я знаю это лучше, чем OCaml, но я считаю, что процесс проверки типов практически одинаковый для двух языков), он позволяет различать эти случаи:

val foo : int = 5
val foo = fn (x) => if x = foo then 0 else 1

Теперь, начиная со второго переопределения, foo имеет тип int -> int. С другой стороны,

val foo : int = 5
val rec foo = fn (x) => if x = foo then 0 else 1

не проверяет тип, потому что rec означает, что typechecker уже решил, что foo отскакивает до типа 'a -> int, и когда он пытается выяснить, что это значит 'a, там является сбоем объединения, потому что x = foo заставляет foo иметь числовой тип, которого нет.

Это может "выглядеть" более насущно, потому что случай без rec позволяет вам делать такие вещи:

val foo : int = 5
val foo = foo + 1
val foo = foo + 1

и теперь foo имеет значение 7. Это не потому, что оно было мутировано, однако --- имя foo было отклонено 3 раза, и так получилось, что каждое из этих привязок затеняет предыдущее связывание переменной с именем foo. Это то же самое, что и:

val foo : int = 5
val foo' = foo + 1
val foo'' = foo' + 1

за исключением того, что foo и foo' больше не доступны в среде после восстановления идентификатора foo. Следующие также являются законными:

val foo : int = 5
val foo : real = 5.0

который дает более четкое представление о том, что происходит затенение исходного определения, а не побочный эффект.

Является ли это стилистически хорошей идеей для повторной проверки идентификаторов, является сомнительным - это может запутать. Это может быть полезно в некоторых ситуациях (например, переименование имени функции для самой версии, которая выводит вывод отладки).

Ответ 6

Я бы сказал, что в OCaml они пытаются сделать REPL, а исходные файлы работают одинаково. Таким образом, совершенно разумно переопределить некоторую функцию в REPL; поэтому они должны разрешить это и в источнике. Теперь, если вы используете (переопределенную) функцию сами по себе, OCaml нуждается в некотором способе узнать, какое из используемых определений: предыдущее или новое.

В Haskell они только что сдались и приняли, что REPL работает в разных версиях от исходных файлов.