Будет ли полезна возможность объявить функции Лиспа «чистыми»?

У вас есть два ответа, но ни один из них не касается реальной проблемы.

Во-первых, да, было бы хорошо знать, что функция чистая. Есть масса вещей на уровне компилятора, которые хотели бы это знать, а также на уровне пользователя. Учитывая, что языки lisp настолько гибки, вы можете немного изменить ситуацию: вместо «чистого» объявления, которое просит компилятор усерднее или что-то в этом роде, вы просто делаете объявление ограничиваете код в определении. . Таким образом, вы можете гарантировать, что функция чистая.

Вы даже можете сделать это с помощью дополнительных вспомогательных средств - я упомянул два из них в комментарии к ответу johanbev: добавьте понятие неизменяемых привязок и неизменяемых структур данных. Я знаю, что в Common Lisp это очень проблематично, особенно неизменяемые привязки (поскольку CL загружает код, "влияя" на его место). Но такие функции помогут упростить вещи, и они не немыслимы (см., например, реализацию Racket с неизменяемыми парами и другими структурами данных и имеет неизменяемые привязки.

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

(define-pure (foo x)
  (cons (+ x 1) (bar)))

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

Теперь начнем с проблем:

1. Он вызывает cons, поэтому предполагает, что он также известен как чистый. Кроме того, как я упоминал выше, он должен полагаться на то, что cons является тем, чем он является, поэтому предположим, что привязка cons неизменна. Легко, так как это известная встроенная функция. Сделайте то же самое с bar, конечно.

2. Но cons имеет побочный эффект (даже если вы говорите о неизменяемых парах Racket): он выделяет новую пару. Это кажется незначительным и игнорируемым моментом, но, например, если вы позволите таким вещам появляться в чистых функциях, то вы не сможете их автоматически запоминать. Проблема в том, что кто-то может полагаться на то, что каждый foo вызов возвращает новую пару, которая не является eq какой-либо другой существующей парой. Кажется, что для того, чтобы все было хорошо, вам нужно еще больше ограничить чистые функции, чтобы они имели дело не только с неизменяемыми значениями, но и со значениями, где конструктор не всегда создает новое значение (например, он может использовать хеш-конусы вместо выделения).

3. Но этот код также вызывает bar, так что вам не нужно делать те же предположения о bar: она должна быть известна как чистая функция с неизменной привязкой. Обратите особое внимание на то, что bar не получает аргументов, поэтому в этом случае компилятор может не только потребовать, чтобы bar была чистой функцией, но и использовать эту информацию и предварительно вычислить ее значение. В конце концов, чистая функция без входных данных может быть сведена к простому значению. (Обратите внимание, кстати, что в Haskell нет функций с нулевым аргументом.)

4. И это приводит к еще одной большой проблеме. Что, если bar является функцией одного входа? В этом случае у вас будет ошибка, и будет выброшено какое-то исключение ... и это уже не чисто. Исключения составляют побочные эффекты. Теперь вам нужно знать арность bar в дополнение ко всему остальному, и вам нужно избегать других исключений. Теперь, как насчет ввода x -- что произойдет, если это не число? Это тоже вызовет исключение, поэтому вам тоже нужно его избегать. Это означает, что теперь вам нужна система типов.

5. Измените это (+ x 1) на (/ 1 x), и вы увидите, что вам нужна не только система типов, но и достаточно сложная, чтобы различать 0.

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

7. Наконец, есть еще один побочный эффект, который остается PITA: что, если определение bar равно (define-pure (bar) (bar))? Это, безусловно, чисто согласно всем вышеперечисленным ограничениям... Но расхождение - это форма побочного эффекта, так что даже это уже не кошерно. (Например, если вы заставили свой компилятор оптимизировать нульарные функции по значениям, то для этого примера сам компилятор застрял бы в бесконечном цикле.) (И да, Haskell не имеет с этим дело, он не делает этого меньше проблем)

Учитывая функцию Лиспа, узнать, чистая она или нет, в общем случае неразрешимо. Конечно, необходимые условия и достаточные условия можно проверить во время компиляции. (Если нечистых операций вообще нет, то функция должна быть чистой; если нечистая операция выполняется безоговорочно, то функция должна быть нечистой; в более сложных случаях компилятор может попытаться доказать, что функция чистая или нечистая. , но не во всех случаях получится.)

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

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

3. Компилятор может либо (а) проверить, действительно ли чистые функции являются чистыми во время компиляции, но в общем случае это неразрешимо, либо (б) добавить код, чтобы попытаться отловить побочные эффекты в чистых функциях во время выполнения и сообщить о них как об ошибке. . (а.) вероятно, было бы полезно с простой эвристикой (например, «нечистая операция выполняется безоговорочно»), (б.) было бы полезно для отладки.

4. Нет, кажется, это имеет смысл. Надеюсь, этот ответ тоже подходит.

Обычные плюсы применяются, когда мы можем предположить чистоту и ссылочную прозрачность. Мы можем автоматически запоминать горячие точки. Мы можем автоматически распараллелить вычисления. Мы можем справиться со многими условиями гонки. Мы также можем использовать совместное использование структур с данными, которые, как мы знаем, не могут быть изменены, например, (квази) примитиву ``cons()'' не нужно копировать cons-ячейки в списке, к которому он относится. На эти клетки никак не влияет наличие другой cons-ячейки, указывающей на них. Этот пример довольно очевиден, но компиляторы часто хорошо разбираются в более сложном совместном использовании структур.

Однако на самом деле определить, является ли лямбда (функция) чистой или имеет ссылочную прозрачность, в Common Lisp очень сложно. Помните, что funcall (foo bar) начинается с просмотра (symbol-function foo). Итак, в этом случае

(defun foo (bar)
  (cons 'zot bar))

foo() чистый.

Следующая лямбда тоже чистая.

(defun quux ()
 (mapcar #'foo '(zong ding flop)))

Однако позже мы можем переопределить foo:

(let ((accu -1))
 (defun foo (bar)
   (incf accu)))

Следующий вызов quux() уже не является чистым! Старый чистый foo() был переопределен в нечистую лямбду. Угу. Этот пример может быть несколько надуманным, но нередко лексически переопределяют некоторые функции, например, с помощью блока let. В этом случае невозможно узнать, что произойдет во время компиляции.

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

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