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

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

S>>Это следует из твоего подхода. Ведь не я, а именно ты предлагаешь судить о чистоте функции по выхлопу виртуальной машины. Вот и ответь себе, бывают ли чистые функции при таком подходе к проверке чистоты?

ARK>Чистых функций, согласно определению из википедии (а не моему подходу), не бывает. Согласно этому определению, говорить можно только чистых ВЫЗОВАХ, а понять чистоту или грязноту самой функции — невозможно.

Вау. Других слов нет.

ARK>Согласно моему подходу, чистые функции — это те функции, которые мы ДЕКЛАРИРОВАЛИ как чистые. Чисты ли будут вызовы таких функций, или не чисты — неважно.
ARK>Соответственно, "декларативно чистая" функция — это функция, которая задекларирована как чистая. Во всех известных мне языках под "чистыми" функциями понимаются именно "декларативно чистые".

Во всех известных мне языках (их не так много) вряд ли пользуются ТВОИМ определением чистоты.

ARK>Декларировать чистоту функции можно несколькими способами.

ARK>1) Сигнатура функции. Самый надежный способ. Встроенные функции имеют сигнатуру, заданную аксиоматически, а построенные поверх них — уже определенную из исходного кода тел этих функций. Варианты сигнатур: ключевое слово "pure" в D, IO-монада в Haskell (декларируется наоборот грязь), "function" в Ada-83 и т.д.

ARK>2) Документация. Из сигнатуры понять нельзя, но в документации явно указано, что функция чиста (декларативно, разумеется!). Менее надежный способ, т.к. компилятор нам уже ничего не подскажет, если документация устарела.

ARK>3) Просмотр исходного кода / вера / чуйка / etc. Самый ненадежный способ. Мы имеем некоторые основания предполагать, что функция чиста (опять же, декларативно — ибо никто не запретит нам ее запустить в виртуальной машине и получить ввод-вывод на этой якобы чистой функции). Но эти основания не подкреплены ничем.

Какой вообще смысл в проверки чистоты виртуальной машиной, если виртуальная машина может сделать грязным даже пустой файл/лист без функций вовсе?

S>>>>Причем тут вера? В евклидовой геометрии параллельными прямыми на плоскости называются непересекающиеся прямые.
ARK>>>Да. Это задано аксиоматически. То же самое и с чистотой (как минимум на уровне встроенных функций).
S>>Пардон, я в определении чистоты не видел перечня аксиоматически чистых функций. Можешь указать мне на него?

ARK>Почему этот перечень должен там быть? Он не часть определения.
Если он не часть определения, почему ты опираешься на этот перечень?

ARK>>>Ты знаешь постулированную кем-то (декларативную) чистоту синуса. Реальную ты не знаешь. Я могу легко написать свою грязную реализацию синуса.
S>>Я знаю, потому нет смысла говорить о чистоте всех синусов. Но с процедурой определения чистоты синуса мне как бы все понятно.

ARK>И каким же образом? Открыл его код, ищешь там функции, которые считаешь грязными (почему ты их считаешь грязными, отдельный вопрос)? Запустил, ожидаешь вывод картинки на принтер или вывод в консоль? Предположим, не увидел ни того, ни другого. Все, после этого ты ВЕРИШЬ, что синус чист? Я правильно описал процедуру определения чистоты?

Немного не так. Я смотрю на контракт, чист ли он? Если синус отличается от своего контракта, то это проблема частной реализации синуса, а не контракта. Если это так — возьму другой.

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

ARK>Кроме контракта, ни о каких вариантах чистоты судить или нет смысла, или невозможно. Контракт может быть задан разными способами (см. выше).

Ну как, ты же судишь по виртуальной машине!

ARK>>>Оно не гадит в момент связывания. А гадит, когда "внешний вычислитель" это запустит. В точности, как в хаскеле.
S>>Передает ли внешний вычислитель при этом управление printf-у? Если да, то грязь появляется до или после возврата управления?

ARK>Идеологически — не передает, а передает управление action'у, который вернул printf. Ой, а как же напрямую вызвать action, который возвращает printf, как это выразить в коде? Никак. Ровно то же самое, что в хаскеле.
А в какой момент action получит строку для вывода, сгенерированную в рантайме?

S>>Давай попробуем разобраться хотя бы в чистоте контракта State. Нужна ли грязь для его реализации?

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

S>>Нужна ли грязь для его реализации?

ARK>Нужна, для телеметрии. Я разработчик нового компилятора Haskell и хочу дать пользователям возможность писать такие программы, активность которых можно при желании контролировать удаленно.
Интересно, что мешает пользователям контролировать активность без нового компилятора? Но ты, видимо, не только компилятор, а еще и все исходники хочешь переписать. Ну ладно. Успехов.