Понимание выражения recurive let в лямбда-исчислении с помощью языков Haskell, OCaml и nix

#haskell #nix #letrec

#haskell #nix #letrec

Вопрос:

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

Я могу найти его в wiki. Для этого мне нужно знать Y-комбинатор, фиксированную точку. Я могу кратко изложить это в wiki.

Затем, теперь я начинаю применять это в Haskell.

Haskell

Это просто. Но я хочу знать за кулисами.

 *Main> let x = y; y = 10; in x
10
 

Комментарии:

1. Вы хотите использовать переменную перед тем, как присвоить ей значение?

2. @Шон, Да. В наборе nix , если нет rec , он не знает переменную, которая будет назначена позже.

3. Я почти уверен, что вы не можете сделать это в ocaml.

4. @Shawn Из-за нетерпеливой оценки ? как Java, C , Python?

5. Когда вы говорите: «Я пытаюсь понять, как рекурсивный набор работает в functional (а не только проверка области видимости).», Я не понимаю, что вы имеете в виду. Вы имеете в виду «работать функционально» или «работать на функциональных языках»? И как вы подразумеваете «работать»; например, «как я могу использовать» или «какова операционная семантика» или «как это работает внутри»?

Ответ №1:

Когда вы пишете a = f b на ленивом функциональном языке, таком как Haskell или Nix, смысл сильнее, чем просто присваивание. a и f b будет то же самое. Обычно это называется привязкой.

Я сосредоточусь на примере Nix, потому что вы спрашиваете конкретно о рекурсивных множествах.

Простой набор атрибутов

Давайте сначала рассмотрим инициализацию набора атрибутов. Когда интерпретатору Nix предлагается оценить этот файл

 { a = 1   1; b = true; }
 

он анализирует его и возвращает структуру данных, подобную этой

 { a = <thunk 1>; b = <thunk 2>; }
 

где thunk — это ссылка на соответствующий узел синтаксического дерева и ссылка на «среду», которая ведет себя как словарь от идентификаторов до их значений, хотя и реализована более эффективно.

Возможно, причина, по которой мы оцениваем этот файл, заключается в том, что вы запросили nix-build , который не просто запросит значение файла, но и пересечет набор атрибутов, когда увидит, что он равен единице. Поэтому nix-build будет запрашиваться значение a , которое будет вычислено из его thunk . Когда вычисление завершено, памяти, в которой хранится блок, присваивается фактическое значение, type = tInt , value.integer = 2 .

Набор рекурсивных атрибутов

Nix имеет специальный синтаксис, который сочетает в себе функциональность синтаксиса построения набора атрибутов ( { } ) и let синтаксиса привязки. Это позволяет избежать некоторых повторений при создании наборов атрибутов с некоторыми общими значениями.

Например

 let b = 1   1;
in { b = b; a = b   5; }
 

может быть выражено как

 rec { b = 1   1; a = b   5; }
 

Вычисление работает аналогичным образом.

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

Обратите внимание, что все эти представления могут быть построены при выполнении минимального объема работы.

nix-build обходит наборы атрибутов в алфавитном порядке, поэтому он будет оцениваться a первым. Это элемент, который ссылается на синтаксический узел a и среду с b ним. Для этого требуется вычислить b синтаксический узел (an ExprVar ), который ссылается на среду, где мы находим 1 1 thunk, который tInt , как и раньше, изменяется на a 2 of .

Как вы можете видеть, этот процесс создания блоков, но оценивающий их только при необходимости, действительно ленив и позволяет нам иметь различные языковые конструкции с их собственными правилами определения области видимости.

Реализации Haskell обычно следуют аналогичному шаблону, но могут компилировать код, а не интерпретировать синтаксическое дерево, и полностью разрешать все ссылки на переменные с постоянными смещениями памяти. Nix пытается сделать это в некоторой степени, но он должен иметь возможность использовать строки из-за нежелательного with ключевого слова, которое делает область динамической.

Комментарии:

1. a = a 5; in let b = 1 1; in { b = b; a = a 5; } -> a = b 5; in rec { b = 1 1; a = b 5; } . Зачем a преобразовывать в b ?

2. Я перепутал пример, когда улучшил примеры, чтобы они соответствовали тексту. Исправлено.

Ответ №2:

Я сам догадываюсь о нескольких вещах.

  • На языке оценки eagar я должен объявить, прежде чем использовать его. Итак, порядок объявления прост.
 int x = 10;
int y = x;
 
  • Только для языка Nix

В wiki нет никакого сравнения понятия с Haskell, хотя let ... in оно сравнивается с Haskell.

  • лексическая область

все переменные имеют лексическую область видимости.

  • взаимная рекурсия

https://en.wikipedia.org/wiki/Let_expression#Mutually_recursive_let_expression