Здравствуйте, AlexRK, Вы писали:
ARK>Здравствуйте, samius, Вы писали:
S>>Я понял. Ты предлагаешь один и тот же "синус" выполнить грязно и чисто. Но причем тут "синус"? Ты переключился с чистоты кода на чистоту исполнения.
ARK>Это то, что следует из твоего подхода. Выполняет ли фактически функция ввод-вывод или нет — от нее вообще не зависит. ARK>Так что же тогда такое "чистая функция", по-твоему? Чистых функций, получается, не бывает?
Это следует из твоего подхода. Ведь не я, а именно ты предлагаешь судить о чистоте функции по выхлопу виртуальной машины. Вот и ответь себе, бывают ли чистые функции при таком подходе к проверке чистоты?
S>>Причем тут вера? В евклидовой геометрии параллельными прямыми на плоскости называются непересекающиеся прямые.
ARK>Да. Это задано аксиоматически. То же самое и с чистотой (как минимум на уровне встроенных функций).
Пардон, я в определении чистоты не видел перечня аксиоматически чистых функций. Можешь указать мне на него?
S>>Согласен, по-строгому надо доказывать. Но это может работать в обе стороны. Утверждаешь, что putStr грязная — докажи.
ARK>Либо доказывать, либо постулировать.
ARK>Чтобы утверждать что-либо о putStr, необходимо формализовать определения. Что есть "чистая", что есть "грязная", что есть "вызов", как отделить одно от другого. Иначе можно, жонглируя словами, спорить бесконечно.
У нас нет единого понятийного аппарата. О каком споре речь?
S>>Дак как же не определить? что с синусом-то не понятно?
ARK>Ты знаешь постулированную кем-то (декларативную) чистоту синуса. Реальную ты не знаешь. Я могу легко написать свою грязную реализацию синуса.
Я знаю, потому нет смысла говорить о чистоте всех синусов. Но с процедурой определения чистоты синуса мне как бы все понятно.
ARK>Это нормально и этого никак не избежать. И это не отменяет полезности декларативного разделения. И твое "правильное" определение не дает никакого лекарства от этого, потому что мы не можем им воспользоваться.
Мы не можем, но я — могу и пользуюсь.
S>>А раз всем пофиг, то вообще какая ТЕБЕ разница, чистая функция или нет?
ARK>Разница такая, что я с ней обращаюсь в коде как с чистой. Я считаю, что ввода-вывода в ней нет, и строю код, исходя из этого предположения. То же самое делает и компилятор, видя флаг "pure" (или отсутствие параметра "IO"). Мой код корректен относительно заданных этой функцией инвариантов. Есть там внутри реально ввод-вывод или нет — меня не интересует. Это слой абстракции. Абстракция позволяет справиться со сложностью и писать корректный код. Если инвариант, предоставляемый функцией, нарушается, то это проблема этой функции, а не моего кода. Я или заменю эту функцию на корректную, или перепишу код иным образом. Проверять контракты всех функций — нелепо. Чистота — это один из контрактов.
Вот это хорошо сказал. Ну то есть, всем не пофиг. Сложно пользоваться функций, если не представляешь или не в полной мере представляешь ее контракты. Что она портит, что берет помимо аргументов, от чего зависит результат (не только лишь возвращаемый, но и изменения в окружении). Т.е. еще один способ судить о чистоте функции (не исчерпывающий, разумеется) — анализ чистоты контракта.
S>>>>Вызов грязной функции не может быть bind-ом, т.к. bind не вызывает ничего, только связывает. ARK>>>Ну а если абстрагироваться и представить, что "f();" — это не вызов, а связывание? S>>Связывание, которое в момент вызова гадит в мир? Давай просто абстрагируемся от того, что f() гадит в мир и скажем, что всем пофиг?
ARK>Оно не гадит в момент связывания. А гадит, когда "внешний вычислитель" это запустит. В точности, как в хаскеле.
Передает ли внешний вычислитель при этом управление printf-у? Если да, то грязь появляется до или после возврата управления?
S>>Ну да почему исходники ничего не дадут? Ты их открывал? Вот открой код манады State и покажи мне в ней грязь.
ARK>Что такое "грязь" в коде? Это вызов функций, которые ты считаешь грязными? А почему ты их считаешь грязными? Потому что это написано в документации?
Давай попробуем разобраться хотя бы в чистоте контракта State. Нужна ли грязь для его реализации?
