Здравствуйте, samius, Вы писали:

ARK>>То и значит. Ты ее не определишь никак, от слова совсем. Причем принципиально, фундаментально, не определишь. Можно взять одну и ту же программу на хаскеле и запустить ее сперва в виртуальной машине, которая выводит на принтер хоста каждое изменение регистров. А потом запустить в другой виртуальной машине, которая блокирует на хосте все запросы на ввод-вывод. В первом случае КАЖДАЯ функция в программе будет грязной. Во втором случае КАЖДАЯ функция в программе будет чистой. Вопрос: каковы же функции в этой программе, грязные или чистые? Программа одна и та же.
S>Я понял. Ты предлагаешь один и тот же "синус" выполнить грязно и чисто. Но причем тут "синус"? Ты переключился с чистоты кода на чистоту исполнения.

Это то, что следует из твоего подхода. Выполняет ли фактически функция ввод-вывод или нет — от нее вообще не зависит.
Так что же тогда такое "чистая функция", по-твоему? Чистых функций, получается, не бывает?

ARK>>Предлагаешь перейти к вере? Представляешь, пишет Пифагор тьфу ты, какой нафиг Пифагор, Евклид конечно на своих скрижалях: я верю, что параллельные прямые не пересекаются. Мамой клянусь, сам видел. Нарисовал километр — не пересеклись. Значит, не пересекаются.
S>Причем тут вера? В евклидовой геометрии параллельными прямыми на плоскости называются непересекающиеся прямые.

Да. Это задано аксиоматически. То же самое и с чистотой (как минимум на уровне встроенных функций).

ARK>>Увы, это так не работает. Есть только два варианта: либо ты постулируешь что-то аксиоматически, либо доказываешь на основе существующих аксиом и теорем. Все, третьего не дано. С чистотой аналогично: либо ты постулируешь чистоту функции, либо доказываешь ее. Вера и чуйка — это не инженерный подход.
S>Согласен, по-строгому надо доказывать. Но это может работать в обе стороны. Утверждаешь, что putStr грязная — докажи.

Либо доказывать, либо постулировать.

Чтобы утверждать что-либо о putStr, необходимо формализовать определения. Что есть "чистая", что есть "грязная", что есть "вызов", как отделить одно от другого. Иначе можно, жонглируя словами, спорить бесконечно.

ARK>>"Истинную" чистоту (чистоту в твоем понимании) не определить никак, ни по исходникам, ни по документации. И лично мне она не нужна. Мне нужна декларативная чистота (обещание компилятора или стандарта языка): либо ключевое слово в исходниках, либо текст в документации. На веру я ничего не принимаю.
S>Дак как же не определить? что с синусом-то не понятно?

Ты знаешь постулированную кем-то (декларативную) чистоту синуса. Реальную ты не знаешь. Я могу легко написать свою грязную реализацию синуса.

S>Ну что, ты на верну ничего не принимаешь, но что если документацию писал человек верующий? Компилятор разрешит unsafe и ты попался со своей декларативной чистотой.

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

ARK>>Не противоречит. Декларируемая чистота нужна для одного: для постулирования и понимания того, что компилятор будет с функцией обращаться как с чистой, невзирая на ее "истинную" чистоту. Это указание компилятору на возможность оптимизации и помощь программисту при чтении исходников. Что там на самом деле происходит — всем пофиг (см. пример выше с виртуальными машинами).
S>А раз всем пофиг, то вообще какая ТЕБЕ разница, чистая функция или нет?

Разница такая, что я с ней обращаюсь в коде как с чистой. Я считаю, что ввода-вывода в ней нет, и строю код, исходя из этого предположения. То же самое делает и компилятор, видя флаг "pure" (или отсутствие параметра "IO"). Мой код корректен относительно заданных этой функцией инвариантов. Есть там внутри реально ввод-вывод или нет — меня не интересует. Это слой абстракции. Абстракция позволяет справиться со сложностью и писать корректный код. Если инвариант, предоставляемый функцией, нарушается, то это проблема этой функции, а не моего кода. Я или заменю эту функцию на корректную, или перепишу код иным образом. Проверять контракты всех функций — нелепо. Чистота — это один из контрактов.

S>>>Вызов грязной функции не может быть bind-ом, т.к. bind не вызывает ничего, только связывает.
ARK>>Ну а если абстрагироваться и представить, что "f();" — это не вызов, а связывание?
S>Связывание, которое в момент вызова гадит в мир? Давай просто абстрагируемся от того, что f() гадит в мир и скажем, что всем пофиг?

Оно не гадит в момент связывания. А гадит, когда "внешний вычислитель" это запустит. В точности, как в хаскеле.

S>>>Ему нет нужды делать грязь, ровно как и синусу. Ну и исходники его на каждом углу. IO в хаскеле реализуется через монаду State, которая чиста как слеза.
ARK>>"Вера" и "чуйка"? Исходники тебе ничего не дадут. Про чистоту монады State тоже вопрос открытый. Ты рассуждаешь о чистоте отдельных функций и понятий аксиоматически, не так ли? Это то, с чего я начал разговор, кстати.
S>Ну да почему исходники ничего не дадут? Ты их открывал? Вот открой код манады State и покажи мне в ней грязь.

Что такое "грязь" в коде? Это вызов функций, которые ты считаешь грязными? А почему ты их считаешь грязными? Потому что это написано в документации?