Может ли чистая функция иметь свободные переменные?

Ответ 1

Насколько я понимаю, "чистота" определяется на уровне семантики, тогда как "ссылочно прозрачная" может воспринимать значение как синтаксически, так и встроенную в правила замены ямбды-исчисления. Определение одного из них также приводит к некоторой сложности в том, что нам нужно иметь надежное представление о равенстве программ, которое может быть сложным. Наконец, важно отметить, что идея свободной переменной полностью синтаксична - как только вы перешли к домену значений, вы больше не можете иметь выражения со свободными переменными - они должны быть связаны иначе, чем синтаксическая ошибка.

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

Quinian Referential Transparency

Мы можем определить ссылочную прозрачность очень широко как свойство синтаксического контекста. По первоначальному определению это будет построено из предложения типа

New York is an American city.

из которых мы выкопали дыру

_ is an American city.

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

Чтобы быть понятным, два фрагмента с той же ссылкой, которую мы можем выбрать, будут "Нью-Йорк" и "Большое яблоко". Вводя эти фрагменты, мы пишем

New York is an American city.
The Big Apple is an American city.

предполагая, что

_ is an American city.

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

"The Big Apple" is an apple-themed epithet referring to New York.

и рассмотрим контекст

"_" is an apple-themed epithet referring to New York.

и теперь, когда мы вставляем две ссылочно идентичные фразы, получаем одно действительное и одно неверное предложение

"The Big Apple" is an apple-themed epithet referring to New York.
"New York" is an apple-themed epithet referring to New York.

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

Синтаксис v Семантика

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

Итак, давайте ясно: существуют два вида ссылочной прозрачности, которые мы можем рассматривать по лямбда-исчислению - синтаксическому и семантическому. Синтаксический требует, чтобы мы определяли "контексты" как дыры в буквальных словах, написанных на языке программирования. Это позволяет нам рассматривать дыры, подобные

let x = 3 in _

и заполнить его такими вещами, как "x". Мы оставим анализ этой замены позже. На семантическом уровне мы используем лямбда-члены для обозначения контекстов

\x -> x + 3         --    similar to the context "_ + 3"

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

(\x -> x + 3) 5 
==> 
5 + 3
==> 
8

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

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

x + 3

на самом деле является синтаксической ошибкой, так как x просто неизвестен, несвязанный, оставляя нас неспособными рассматривать семантику его как программу Haskell. Во-вторых, само понятие переменной, такое как та, которая может быть let -bound (и учитывать разницу между "переменной", поскольку она относится к "слоту", например, IORef), полностью является синтаксической конструкцией - там никоим образом не говорить о них изнутри семантики программы Haskell.

Итак, уточним вопрос:

Может ли выражение, содержащее свободные переменные, (синтаксически) ссылочно прозрачным?

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

Свободные контексты переменных

Как контекст имеет смысл иметь свободную переменную? Это может быть рядом с дырой

E1 ... x ... _ ... E2

и до тех пор, пока мы не можем вставить что-то в эту синтаксическую дыру, которая "достигает" и синтаксически влияет на x, тогда мы в порядке. Так, например, если мы заполняем эту дыру чем-то вроде

E1 ... x ... let x = 3 in E ... E2

то мы не "захватили" x и, следовательно, можем считать, что синтаксическая дыра является ссылочно прозрачной. Тем не менее, мы хорошо относимся к нашему синтаксису. Рассмотрим более опасный пример

do x <- foo
   let x = 3
   _
   return x

Теперь мы видим, что отверстие, которое мы предоставили в некотором смысле, имеет доминирование над более поздней фразой "return x". Фактически, если мы впрыскиваем фрагмент типа "let x = 4", то он действительно меняет смысл целого. В этом смысле синтаксис здесь не является ссылочно прозрачным.

Другим интересным взаимодействием между ссылочной прозрачностью и свободными переменными является понятие присваивающего контекста, такого как

let x = 3 in _

где, с внешней точки зрения, обе фразы "x" и "y" относятся к одной и той же вещи, некоторой именованной переменной, но

let x = 3 in x   ==/==  let x = 3 in y

Прогрессия от колючки вокруг равенства и контекста

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

foo >>= \x -> (let x = 3 in ____(return x)_____)

Является ли это действительным понятием контекста? Это зависит от того, какой смысл мы даем программе. Понятие desugaring синтаксиса уже подразумевает, что синтаксис должен быть достаточно хорошо определен, чтобы допускать такую ​​десурацию.

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

В конечном итоге это приводит нас к тому, что я называл "семантической ссылочной прозрачностью" ранее, когда мы можем только подставить правильные значения в правильное замкнутое лямбда-выражение, и мы принимаем полученное равенство как "равенство как программы".

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

Purity

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

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

trivial :: a -> ()
trivial x = x `seq` ()

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

trivial_Int :: Int -> ()
trivial_Int x = x `seq` ()

Теперь мы можем определить (очень строгую) чистую функцию как функцию f :: a -> b такую, что

trivial_b . f = trivial_a

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

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

Итак, что ответ?

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

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

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

Ответ 2

Определение Википедии является неполным, поскольку чистая функция может использовать константы для вычисления своего ответа.

Когда мы смотрим на

increment n = 1+n

это очевидно. Возможно, это не было упомянуто, потому что это очевидно.

Теперь трюк в Haskell заключается в том, что не только значения верхнего уровня и функции являются константами, но и внутри замыкания также перекрываются переменные (!):

add x = (\y -> x+y)

Здесь x означает значение, которое мы применили add to - мы называем его переменной не потому, что оно может меняться в правой части add, а потому, что оно может быть различным при каждом применении add, И все же, с точки зрения лямбда, x является константой.

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

Ответ 3

Короткий ответ ДА f чистый

В Haskell map определяется foldr. Согласны ли вы, что map является функциональным? Если это имело значение, то он имел глобальную функцию foldr, которая не была передана в map в качестве аргумента?

В map foldr - свободная переменная. Это не вызывает сомнений. Не имеет значения, что это функция или что-то, что оценивает значение. То же самое.

Свободные переменные, такие как функции foldl и +, необходимы для существования функциональных языков. Без этого у вас не было бы абстракции, и языки были бы хуже, чем Фортран.