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