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

Question

В последнее время я много читал о Haskell , и о преимуществах, которые он дает, будучи чисто функциональным языком.(Я не заинтересован в обсуждении монад для Lisp) Для меня имеет смысл (по крайней мере, логически) максимально изолировать функции с побочными эффектами.Я много использовал setf и другие деструктивные функции, и я осознаю необходимость их использования в Лиспе и (большей части) его производных.

Вот так:

1. Может ли что-то вроде (declare pure) потенциально помочь оптимизирующему компилятору?Или это спорный вопрос, потому что он уже знает?
2. Может ли объявление помочь в доказательстве функции или программы или хотя бы подмножества, объявленного чистым?Или это опять то, что не нужно, потому что это уже очевидно для программиста, компилятора и проверяющего?
3. Если бы ни для чего другого, было бы полезно для программиста для компилятора обеспечить принудительную чистоту функций с помощью этого объявления иувеличить читабельность / поддерживаемость программ на Лиспе?
4. Имеет ли что-нибудь из этого смысл?Или я слишком устал, чтобы даже думать прямо сейчас?

Буду признателен за любые идеи здесь.Информация о реализации компилятора или доказуемости приветствуется.

EDIT

Чтобы уточнить, я не собирался ограничивать этот вопрос Common Lisp.Ясно, что это (я думаю) не относится к определенным производным языкам, но мне также любопытно, могут ли некоторые функции других Лиспов поддерживать (или нет) такую ​​возможность.

Answer 1

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Answer 2

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

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

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

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

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

Answer 3

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

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

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