Теория категорий, Haskell и программирование вообще

[alex55555]

(Оффтоп)

arseniiv в сообщении #1377295 писал(а):

можно проверить кодом (undefined :: IO ()) `seq` 1 — undefined вычислится и даст как полагается исключение.

Да, действительно исключение. Но не потому, что seq запускает отложенное вычисление. Undefined в хаскеле эквивалентно понятию bottom, обозначаемому знаком $\perp$. А seq в Haskell Report объявлена так:

Цитата:

seq $\perp$ b = $\perp$
seq a b = b, if a $\ne$ $\perp$

То есть вы в данном случае просто "попали" в нужный диапазон. Случай же со второй ветвью так и остался неисследованным.

arseniiv в сообщении #1377295 писал(а):

Как я уже написал, в подходе, использующем RealWorld, без него нельзя, по определению.

Вы считаете, что в хаскеле используется подход, в котором обязателен RealWorld? Тогда что же будет с памятью при большом количестве ветвей дерева исполнения?

arseniiv в сообщении #1377295 писал(а):

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

Разговор шёл о ленивом IO и его отличии от неленивого. Я показал пример, где на мой взгляд проявлялась ленивость в отношении IO. Далее пошло обсуждение, можно ли это считать проявлением ленивости.

arseniiv в сообщении #1377295 писал(а):

Но он не обязателен, просто если не лезть в реализацию IO, будет и нечем иллюстрировать вам, почему вы должны быть неправы. Можно, конечно, не пытаться ничего иллюстрировать, просто люди попались достаточно добрые.

Не совсем осознал ваш намёк на моё невежество. Раскройте пожалуйста подробнее (как добрый человек для дурака).

arseniiv в сообщении #1377295 писал(а):

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

Могу предположить, что IO предполагает некую последовательность вызовов, скрытую от разработчиков на хаскель, которую seq принуждает не полностью. Но принуждение, вообще говоря, предполагает некий результат и причём сразу. Если он зависит от некой вложенности, то было бы логично на это указать в стандарте языка. Но в стандарте такого указания нет. А приводимый вами пример deepseq относится к специальному типу NFData, который, понятное дело, и не должен никак отражаться в стандарте языка, поскольку является лишь его дополнительной библиотекой (в стандарте из всего пакета Control есть только Monad, и более ничего). И в целом получаем, что seq работает непонятно как, а возможные замены вроде deepseq не описаны в стандарте языка. Разве это хорошая документированность языка?

arseniiv в сообщении #1377295 писал(а):

alex55555 в сообщении #1377258 писал(а):

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

Уверен, что в упомянутом вами Haskell Report 2010 вот так не написано, а написано конкретнее (по идее про WHNF должно быть сказано).

Там помимо неформального определения seq есть ещё напоминание о ленивости языка и такое указание:

Цитата:

Sometimes it is desirable to force the evaluation of a value, using the seq function:

Используется синтаксис Haskell

seq :: a -> b -> b

Остальное - краткие рассуждения о предназначении seq для обхода ленивости и некоторые семантические свойства bottom, далее про операторы $ и (тоже знак доллара, а затем !, но второй знак подряд некорректно воспринимается форумом), а так же их семантические различия.

arseniiv в сообщении #1377295 писал(а):

alex55555 в сообщении #1377258 писал(а):

Вот опять - принуждение должно приводить к мгновенному исполнению, а вы говорите об отложенном исполнении. Поэтому я не понимаю смысла слова "форсить".

Ну в принципе тут может быть непонимание, если позволить IO a быть просто банально обёрткой над a (но никто вроде так не делает). Тогда если бы мы зафорсили некое значение IO a, его эффекты бы выполнились.

Пусть обёртка "непростая", но смысл операций с ней где-то надо бы пояснять. И даже скорее всего где-то такое пояснение есть, но вот как бы его найти при возникновении такой необходимости? Разве само появление такого вопроса не говорит о плохом документировании хаскеля?

arseniiv в сообщении #1377295 писал(а):

Ещё раз, в наивном понимании значение типа IO a — это лишь описание того, что надо сделать, и что должно вернуть a, если не будет исключений. Зафорсим мы выражение, дающее такое описание в результате — разумеется, ничего не будет выполнено волшебным образом. Мы просто получим описание в WHNF (то есть даже не полностью до всех-всех конструкторов развёрнутое). Почему вы это игнорируете, непонятно.

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

Про наивное понимание у меня своя версия, но похоже вам она не нравится :) Пока было бы неплохо получить какое-то описание того, что происходит при попытке отдать IO в виде левого аргумента в seq. Если вы может привести такие детали, то буду очень благодарен. Тем более, что вы вроде заикнулись:

arseniiv в сообщении #1377295 писал(а):

Если же вам не нравится аргумент от наивного описания, то надо поднять уровень разговора и говорить в любом случае более специфично.

arseniiv в сообщении #1377295 писал(а):

alex55555 в сообщении #1377258 писал(а):

Мне кажется, это не проблема монад или апликативов, а проблема хаскеля. Банально - он плохо документирован.

Это уход в сторону. Очень надеюсь, что вы делаете такое раз за разом не сознательно.

Обсуждение под тэгом offtopic обычно как раз туда и уходят. Хотя признаюсь, вы первый закрыли это дело под спойлер, но я вашим заветам честно следую :)

arseniiv в сообщении #1377295 писал(а):

alex55555 в сообщении #1377258 писал(а):

При этом Haskel Report даёт лишь намёки, но никакой конкретики, ссылаясь на свободу реализации, поэтому нужно изучать реальное устройство компилятора, которых несколько, что очевидно - несколько кривой подход.

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

Я понимаю, что вам не интересен вопрос документирования, но так уж получилось, что в ответе на ваше высказывание я увидел вполне логически подходящее место для указания на более общую проблему, нежели просто различие между монадами и аппликативами.

[arseniiv]

(Оффтоп)

Да, к сожалению в Report 2010 нет про доведение до WHNF, ну остаётся только оставить заметку комитету, который будет писать report следующей версии.

alex55555 в сообщении #1377346 писал(а):

Но не потому, что seq запускает отложенное вычисление. Undefined в хаскеле эквивалентно понятию bottom, обозначаемому знаком $\perp$. А seq в Haskell Report объявлена так: <…>

Это одно и то же. Нельзя определить seq как-то иначе*, чтобы для неё были справедливы эти равенства, ибо мы не можем узнать, $\bot$ ли какое-то значение, но «скопировать» $a=\bot$ мы можем, выполнив a перед или после чего-то. Чтобы в a `seq` b = b в противном случае, нам надо вычислять b тоже, притом после a (если вычислять b перед a, получим flip seq вместо seq).

* Точнее, как-то значительно иначе. Пишут, что этих равенств недостаточно для однозначного определения. Однако необходимость вычислять первый аргумент и второй после него никуда не девается.

alex55555 в сообщении #1377346 писал(а):

Вы считаете, что в хаскеле используется подход, в котором обязателен RealWorld? Тогда что же будет с памятью при большом количестве ветвей дерева исполнения?

Я считаю, что не важно что используется (но GHC действительно передаёт такой токен длины, как пишут, 0). А с памятью от этого должно что-то особенное случаться?

alex55555 в сообщении #1377346 писал(а):

Я показал пример, где на мой взгляд проявлялась ленивость в отношении IO. Далее пошло обсуждение, можно ли это считать проявлением ленивости.

Да, и остаётся только повторить, что seq форсит свой левый аргумент и потому говорить в том примере о ленивости как минимум самонадеянно.

alex55555 в сообщении #1377346 писал(а):

Не совсем осознал ваш намёк на моё невежество. Раскройте пожалуйста подробнее (как добрый человек для дурака).

Ну вам уже целую страницу раскрывали, что вы неправильно понимаете про seq, и намёков тоже никаких нет, насчёт неправоты сказали явно и первым даже не я.

alex55555 в сообщении #1377346 писал(а):

Но принуждение, вообще говоря, предполагает некий результат и причём сразу. Если он зависит от некой вложенности, то было бы логично на это указать в стандарте языка. Но в стандарте такого указания нет. А приводимый вами пример deepseq относится к специальному типу NFData, который, понятное дело, и не должен никак отражаться в стандарте языка, поскольку является лишь его дополнительной библиотекой (в стандарте из всего пакета Control есть только Monad, и более ничего). И в целом получаем, что seq работает непонятно как, а возможные замены вроде deepseq не описаны в стандарте языка. Разве это хорошая документированность языка?

Не собираюсь обсуждать документированность, но есть причины не лезть внутрь конструкторов. Тогда вычисление завершается, когда определён конструктор (и если у него строгие !-поля, зафоршены и они). В любом случае, пару вещей можно вывести и из того определения seq, что дано в Report, и они не согласуются с вашей гипотезой, всё.

alex55555 в сообщении #1377346 писал(а):

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

А то, что уже было упомянуто, недостаточно? Хоть скажите, почему именно. А то вот я лично когда читаю, не вижу, чтобы вы писали что-то существенно новое. Потом ещё про документацию снова начали — ну допустим даже она была бы вообще никакая, как это относится сюда? Даже если нужно читать другие источники, и если её недостаточно, чтобы разбираться в хаскеле, это не изменит контекста никак.

alex55555 в сообщении #1377346 писал(а):

Пока было бы неплохо получить какое-то описание того, что происходит при попытке отдать IO в виде левого аргумента в seq. Если вы может привести такие детали, то буду очень благодарен. Тем более, что вы вроде заикнулись:

arseniiv в сообщении #1377295 писал(а):

Если же вам не нравится аргумент от наивного описания, то надо поднять уровень разговора и говорить в любом случае более специфично.

1. Ну так описано же, что она делает: она вычисляет; до того, пока не наткнётся на конструктор (здесь один из конструкторов IO) или недоприменённую функцию, после чего заканчивает (ибо WHNF). Эффекты выполнять она не будет, этим рантайм занимается на отдельных началах, а не в качестве вычислений, хоть бы и вычислений с участием seq.
2. Я лично уровень и так уже пару раз вверх подёргал, всё вроде без толку.

alex55555 в сообщении #1377346 писал(а):

Обсуждение под тэгом offtopic обычно как раз туда и уходят.

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

alex55555 в сообщении #1377346 писал(а):

Я понимаю, что вам не интересен вопрос документирования

Интересен, но не в текущем контексте.

alex55555 в сообщении #1377346 писал(а):

но так уж получилось, что в ответе на ваше высказывание я увидел вполне логически подходящее место для указания на более общую проблему, нежели просто различие между монадами и аппликативами.

А никто вроде и не говорил, что это язык без проблем. Вопрос, зачем упоминать просто так, остаётся. Не знаю как остальные, а мне трудно управляться с одним только этим разговором про seq без отступлений. Опять же, контекст: иногда дополнения по ассоциациям могут принести гипотетическую пользу, например если темой было какое-то абстрактное X и дополнение касается примеров разных конкретных X. (И по крайней мере под этот шаблон отступления про качество документации вообще не подходят.)

[alex55555]

(Оффтоп)

arseniiv в сообщении #1377382 писал(а):

Нельзя определить seq как-то иначе*, чтобы для неё были справедливы эти равенства

Здесь всё упирается в лямбда исчисление и, возможно, другие математические теории. Вы здесь на своём поле, я же не математик. Поэтому можно или нельзя определить в математических терминах - не знаю. Но знаю точно, что можно определить алгоритмически. Причём абсолютно однозначно и очень коротко.

Из этого есть следствие - если для понимания двух строк алгоритма нужно изучить лямбда исчисления и ещё что-то, то на мой взгляд это как раз напрямую относится к вопросу, заданному автором темы. Он спросил про смысл изучения теории категорий в применении к хаскелю и программированию вообще, но часть "в применении к хаскелю", как мы видим, просто невозможна в полном виде без изучения ещё и лямбда исчисления (и возможно чего-то ещё).

Но вам спасибо, что хоть и несколько нетерпеливо, но наглядно показали и это важный момент, переводящий "игры с хаскелем" в ещё более затяжное занятие.

arseniiv в сообщении #1377382 писал(а):

Я считаю, что не важно что используется (но GHC действительно передаёт такой токен длины, как пишут, 0). А с памятью от этого должно что-то особенное случаться?

То, что используется, определяется некой целью. Разговор начался с недостающего параметра RealWorld, который по мнению участников не даёт исполнять операции с эффектами. Я заметил, что если бы это было так, то программам очень часто не хватало бы памяти. Поэтому я считаю, что параметр RealWorld служит для каких-то других целей, которые нужно выяснять где-то в описании компиляторов хаскеля. Ну а передаётся он или нет, это действительно не важно в сравнении с темой о том, как этот параметр используется.

arseniiv в сообщении #1377382 писал(а):

alex55555 в сообщении #1377346 писал(а):

Я показал пример, где на мой взгляд проявлялась ленивость в отношении IO. Далее пошло обсуждение, можно ли это считать проявлением ленивости.

Да, и остаётся только повторить, что seq форсит свой левый аргумент и потому говорить в том примере о ленивости как минимум самонадеянно.

Хорошо, заменим seq самописной функцией, возвращающей второй параметр и игнорирующей первый. Проявится ли здесь ленивость?

На seq я остановился почти случайно, просто вспомнив её в вашем же сообщении и использовав в роли функции, игнорирующей первый параметр. Хотя да, в глубины понимания лямбда исчисления при этом я совершенно не вдавался. Ну а отсутствие принуждения проверил экспериментально. Как минимум - эффект выглядит именно так (если не вдаваться в лямбда исчисления).

arseniiv в сообщении #1377382 писал(а):

Ну вам уже целую страницу раскрывали, что вы неправильно понимаете про seq.

Хорошо, признаю, что в лямбда исчислениях не силён. Но алгоритмический смыл хотелось бы видеть. И что важно - этот смысл реально есть (реализован в компиляторе), но сокрыт за мраком лямбда исчисления.

arseniiv в сообщении #1377382 писал(а):

В любом случае, пару вещей можно вывести и из того определения seq, что дано в Report, и они не согласуются с вашей гипотезой, всё.

Не заметил этой пары вещей. В сети пишут, что seq действительно принуждает, но как - совершенно не понятно. Остаётся лишь гадать на тему того, как конкретно выглядит объект IO или же функции, его возвращающие, от чего далее строить гипотезы о работе seq. Только все эти гадания могли бы быть сведены к нулю, будь у хаскеля нормальная документация.

arseniiv в сообщении #1377382 писал(а):

Потом ещё про документацию снова начали — ну допустим даже она была бы вообще никакая, как это относится сюда?

Если она никакая, то не возникает понимания модели исполнения. А без такого понимания невозможно полноценно использовать инструмент. Ссылки же на лямбда исчисления и прочую математику совсем не добавляют понятности в использовании инструмента, а лишь заставляют тратить на его изучение всё больше и больше времени (по сути вместо хаскеля изучая почти всю математику). Разве это нормально? Ну и разве не стоит ответить автору темы именно с указанием на такие потенциальные сложности?

arseniiv в сообщении #1377382 писал(а):

Ну так описано же, что она делает: она вычисляет; до того, пока не наткнётся на конструктор (здесь один из конструкторов IO) или недоприменённую функцию, после чего заканчивает (ибо WHNF).

А почему вы считаете, что IO отдаётся функцией putStr в неком разобранном состоянии? В смысле зачем применять конструктор к уже созданному объекту?

Мне кажется, что никакие недоприменённые функции и прочее здесь никак не участвуют, но просто не выполняется операция, которую putStr положило в объект IO. И недовыполняется она из-за специфической реализации работы с эффектами, создание которых рантайм планирует по своим законам. Законы нам неизвестны, но нам вполне известен ленивый механизм задержки исполнения, используемый в хаскеле, поэтому логично предположить, что именно лень в данном случае всё же играет важнейшую роль - она не даёт рантайму повода для запуска эффектов. То есть объект IO никто не дёргает, а ленивость, соответственно, предполагает отсутствие исполнения в таком случае.

Ваша же версия про конструктора и прочее совершенно не укладывается в имеющиеся у нас факты. А вот с ленивостью - всё становится понятным.

arseniiv в сообщении #1377382 писал(а):

Эффекты выполнять она не будет, этим рантайм занимается на отдельных началах, а не в качестве вычислений, хоть бы и вычислений с участием seq.

Роль seq здесь - принуждение. Но как мы наблюдаем - принуждение не сработало, не смотря на то, что хоть оно и выполнилось (множество заявлений в интерентах тому подтверждение), но скорее всего само выполнение не предполагало создание эффекта именно до наступления события, когда этот эффект будет востребован в каком-то внешнем вызове, то есть до выполнения "ленивых" правил.

arseniiv в сообщении #1377382 писал(а):

Обсуждение seq в этой теме оффтоп, обсуждение качества документации — оффтоп по отношению к этому оффтопу, и я по одной из предыдущих тем с вашим участием уже уяснил, что почкуются они как гидра.

Глубокое понимание вопроса требует, например, изучения всей математики, но мне не приходит в голову заявлять, что это оффтоп и потому я не буду ничего изучать.

Автор темы спросил - что даст изучение теории категорий и хаскеля для программиста? И весь наш разговор прямым текстом ему сообщает - изучение даст возможность надолго погрязнуть в глубинах математики с совершенно непонятным результатом на выходе. По мне так это очень важная для автора темы информация.

arseniiv в сообщении #1377382 писал(а):

Не знаю как остальные, а мне трудно управляться с одним только этим разговором про seq без отступлений.

Ну вот и вы тоже понимаете, что показать что-то серьёзное не вникая в глубины - невозможно. Я рад такой внезапной поддержке с вашей стороны :)

[_Ivana]

(Оффтоп)

У меня нет слов, лишь немое восхищение! Впрочем, некоторое количество слов по данному вопросу можно позаимствовать у классика А. П. Чехов. Письмо к ученому соседу

[Xaositect]

(Оффтоп)

По-моему, Haskell report достаточно ясен в этом плане:

Цитата:

A value of type IO a is a computation which, when performed, does some I/O before returning a value of type a.

There is really only one way to ”perform” an I/O action: bind it to Main.main in your program. When your program is run, the I/O will be performed. It isn’t possible to perform I/O from an arbitrary function, unless that function is itself in the IO monad and called at some point, directly or indirectly, from Main.main.

Откуда следует, что вычисление аргумента (force evaluation), которое производит seq, и выполнение IO (perform) - это разные вещи. Значения типа IO a - это некоторое представление действий, которые могут быть выполнены программой. Действие, которое программа действительно выполняет - это, по стандарту, только main (по факту есть еще unsafePerformIO).

К lazy IO это, кстати, не имеет никакого отношения.

[arseniiv]

(Оффтоп)

alex55555 в сообщении #1377442 писал(а):

Но знаю точно, что можно определить алгоритмически. Причём абсолютно однозначно и очень коротко.

По определению из Report? Если вы умеете матчить $\bot$, тогада да, но это же проблема остановки. Если у вас там рядом есть гипертьюринговская вычислялка, чтобы это не было проблемой, не тратьте её ресурсы зря на определение какого-то seq, у неё есть куда более полезные применения.

alex55555 в сообщении #1377442 писал(а):

Хорошо, заменим seq самописной функцией, возвращающей второй параметр и игнорирующей первый. Проявится ли здесь ленивость?

То есть заменить seq на flip const; да, тогда первый аргумент не вычислится вообще никогда, опять же вне зависимости от того кто он. А про отношение всего этого к lazy I/O уже говорили.

alex55555 в сообщении #1377442 писал(а):

Хотя да, в глубины понимания лямбда исчисления при этом я совершенно не вдавался.

Да нет там никаких глубин, ну честно. Неправильно заложенные основы вот могут быть, иначе само бы всё образовалось по необходимости.

alex55555 в сообщении #1377442 писал(а):

Но алгоритмический смыл хотелось бы видеть. И что важно - этот смысл реально есть

См. выше много раз. Приводит первый аргумент к WHNF, после этого второй. Рантайм оперирует выражениями-графами, в этом контексте это прекрасная операционная семантика.

alex55555 в сообщении #1377442 писал(а):

В сети пишут, что seq действительно принуждает, но как - совершенно не понятно.

В той же сети пишут, что к WHNF.

alex55555 в сообщении #1377442 писал(а):

Если она никакая, то не возникает понимания модели исполнения. А без такого понимания невозможно полноценно использовать инструмент. Ссылки же на лямбда исчисления и прочую математику совсем не добавляют понятности в использовании инструмента, а лишь заставляют тратить на его изучение всё больше и больше времени (по сути вместо хаскеля изучая почти всю математику). Разве это нормально? Ну и разве не стоит ответить автору темы именно с указанием на такие потенциальные сложности?

Про последнее: ну в основном вопрос автора был о связи хаскеля и теории категорий, и как сам же автор писал, достаточно внятно он задать его к тому моменту не мог. Это не значит, что надо злоупотреблять этой недосказанностью, разведя вот такое количество оффтопа как получилось. Ну ей-богу.

Про первое: вообще-то полно инструментов, правильное использование которых изучать ещё дольше, и не потому что кто-то где-то не умеет писать, а потому что долго в голову укладывать. И кстати странно говорить, что нужно пытаться обойтись без знания λ-исчисления, когда хаскель — один из «наиболее функциональных» языков. Языки не равноценны, хаскель не бейсик. (И продолжать эту часть, как уже говорил, не буду.)

alex55555 в сообщении #1377442 писал(а):

А почему вы считаете, что IO отдаётся функцией putStr в неком разобранном состоянии? В смысле зачем применять конструктор к уже созданному объекту?

Не понимаю, что вы написали про конструктор. Он не применяется к созданному. Когда мы вычисляем выражение, мы можем узнать, что оно является «конечными данными», а именно узнать, что это конструктор данных, применённый к каким-то аргументам. Если в описании типа данных у этого конструктора нет строгих полей, на этом вычисление и закончится. В зависимости от того как устроен IO a, при вычислении putStr s может получиться, скажем, какое-нибудь IOPrimitivePutStr s или что-то другое.

alex55555 в сообщении #1377442 писал(а):

Мне кажется, что никакие недоприменённые функции и прочее здесь никак не участвуют, но просто не выполняется операция, которую putStr положило в объект IO.

Что это значит в терминах хаскеля? Как можно что-то положить в какой-то объект?

alex55555 в сообщении #1377442 писал(а):

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

Ещё раз, если бы хаскель был строгим, но имел такую же реализацию I/O, при выполнении action1 `seq` action2 выполнялось бы так же только action2. Когда нужно, чтобы они выполнялись оба и в последовательности, пишут action1 >> action2.

alex55555 в сообщении #1377442 писал(а):

Но как мы наблюдаем - принуждение не сработало

Отправляйте багрепорт тем, кто пишет используемый вами компилятор.

alex55555 в сообщении #1377442 писал(а):

И весь наш разговор прямым текстом ему сообщает - изучение даст возможность надолго погрязнуть в глубинах математики с совершенно непонятным результатом на выходе.

Если вы хотели показать, что у автора есть вероятность* погрязнуть — это вы уже показали более чем достаточно, можно было так долго не продолжать. (*Без дополнительных обоснований трудно утверждать, достаточно ли большая.)

alex55555 в сообщении #1377442 писал(а):

Ну вот и вы тоже понимаете, что показать что-то серьёзное не вникая в глубины - невозможно.

Нет, я имел в виду, что конкретно такое развёртывание обсуждения для меня лично очень затратное дело (почему-то с вами оно каждый раз такое, вот странные совпадения). Засим перехожу в R/O.

[alex55555]

(Оффтоп)

Увидел отказ от продолжения, но тем не менее по заявленным обвинениям отвечу.

arseniiv в сообщении #1377471 писал(а):

alex55555 в сообщении #1377442 писал(а):

Но знаю точно, что можно определить алгоритмически. Причём абсолютно однозначно и очень коротко.

По определению из Report?

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

arseniiv в сообщении #1377471 писал(а):

Если вы умеете матчить $\bot$, тогада да, но это же проблема остановки.

Значение undefined несколько отличается от проблемы остановки. Теоретическая база здесь немного "не так" работает. Есть конкретная (и простая) реализация и есть некая абстракция из лямбда исчисления, последнее вы выдаёте за истину, а первого просто не замечаете. Но в реальности работает именно первое, и ему не нужно ничего более, чем пара строчек кода.

arseniiv в сообщении #1377471 писал(а):

да, тогда первый аргумент не вычислится вообще никогда, опять же вне зависимости от того кто он. А про отношение всего этого к lazy I/O уже говорили.

Ну вот, если первый аргумент не вычисляется, то вы продолжаете настаивать, что лень здесь ни при чём? Я уж не знаю, возможно вам стоит напомнить определение ленивых вычислений. Хотя возможно вас ввело в заблуждение упоминание lazy IO (не мной), но это опять другая тема, другой пакет, другая реализация. По простому - lazy IO не равно обычному IO.

arseniiv в сообщении #1377471 писал(а):

Да нет там никаких глубин, ну честно. Неправильно заложенные основы вот могут быть, иначе само бы всё образовалось по необходимости.

Ну вам виднее, но изучать-то надо? Тогда против чего вы возражали? По сути вы утверждаете, что для изучения хаскеля нет никаких проблем поизучать ещё и всю математику, ведь там нет никаких глубин.

arseniiv в сообщении #1377471 писал(а):

alex55555 в сообщении #1377442 писал(а):

В сети пишут, что seq действительно принуждает, но как - совершенно не понятно.

В той же сети пишут, что к WHNF.

Вопрос был о понимании конкретного способа работы программы. Теоретическое понимание на тему "принуждать пока принуждается" (если перевести WHNF на русский) ничем не помогает пониманию конкретного способа работы программы. Если нет понимания, как работает программа, то и сделать что-то осмысленное она, весьма вероятно, не сможет. Поэтому ваше предложение "расшифровать" действия программы ссылкой на WHNF приведёт лишь к неработоспособности программы.

arseniiv в сообщении #1377471 писал(а):

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

Вообще - можно спросить у автора. Если ему не нравится, он мог бы об этом сообщить и я бы отошёл от этой беседы. Но ваше указание на ваше мнение о мнении автора я всё же не воспринимаю как приказ к остановке. Тем более, что в нашем с вами обсуждении есть весьма важные моменты, которые вы старательно переводите в обвинение в невежестве. Я же пока надеялся на некоторую непредвзятость, но вы пресекаете любые попытки копнуть глубже ссылками на оффтоп, чего я совершенно не разделяю, ибо вижу в этом не самые хорошие желания. Если вас утомило что-то объяснять, гораздо проще было бы не отвечать вообще, или отвечать лишь на те моменты, которые вам интересны. Но пока вы отвечаете, да ещё и в виде обвинений в невежестве, мне приходится оправдываться.

arseniiv в сообщении #1377471 писал(а):

Про первое: вообще-то полно инструментов, правильное использование которых изучать ещё дольше, и не потому что кто-то где-то не умеет писать, а потому что долго в голову укладывать.

Это никак не оправдывает наличие проблем в хаскеле.

arseniiv в сообщении #1377471 писал(а):

И кстати странно говорить, что нужно пытаться обойтись без знания λ-исчисления, когда хаскель — один из «наиболее функциональных» языков.

Я говорил, что нужно изучать лямбда исчисление для понимания хаскеля. Зачем же так откровенно искажать?

arseniiv в сообщении #1377471 писал(а):

В зависимости от того как устроен IO a, при вычислении putStr s может получиться, скажем, какое-нибудь IOPrimitivePutStr s или что-то другое.

Не важно, что получается на выходе putStr, важно, что это что-то не приводит к появлению эффекта, а это и есть (по определению) признак ленивости.

arseniiv в сообщении #1377471 писал(а):

alex55555 в сообщении #1377442 писал(а):

Мне кажется, что никакие недоприменённые функции и прочее здесь никак не участвуют, но просто не выполняется операция, которую putStr положило в объект IO.

Что это значит в терминах хаскеля?

putStr создаёт объект, содержащий информацию о требуемом вычислении, но не содержащий результатов требуемого вычисления.

arseniiv в сообщении #1377471 писал(а):

Как можно что-то положить в какой-то объект?

Это называется присваивание значения ссылочному типу данных.

arseniiv в сообщении #1377471 писал(а):

alex55555 в сообщении #1377442 писал(а):

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

Ещё раз, если бы хаскель был строгим, но имел такую же реализацию I/O, при выполнении action1 `seq` action2 выполнялось бы так же только action2.

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

arseniiv в сообщении #1377471 писал(а):

я имел в виду, что конкретно такое развёртывание обсуждения для меня лично очень затратное дело (почему-то с вами оно каждый раз такое, вот странные совпадения).

Когда истина скрыта в глубинах формализмов, приходится глубоко копать. Но да, это затратно.

[arseniiv]

(Оффтоп)

alex55555 в сообщении #1377542 писал(а):

Сарказм здесь ни к чему, определение вы видели, смысл отлично поняли.

Это был не сарказм, я просто не воспринимаю то определение как «алгоритмическое». Потому что мы не можем сделать такой матчинг, как я уже писал. Так что перевести это в код прозрачным образом нельзя.

А то, что достаточно, я не отрицаю. Изначально вы просто сказали, что «мне повезло» с undefined `seq` ..., потому-то я и пояснил, что не повезло, а так и должно быть. После чего вы, вероятно, забыли контекст. (И немудрено; разговоры стараются не разветвлять сверх меры и потому, чтобы люди могли удержать в памяти, о чём же они говорят.)

alex55555 в сообщении #1377542 писал(а):

Ну вот, если первый аргумент не вычисляется, то вы продолжаете настаивать, что лень здесь ни при чём?

Не смешивайте одно с другим. Я говорил, что лень ни при чём в примере с seq.

Одно и то же по десятому кругу. Кто-то из нас не умеет читать.

[warlock66613]

(Оффтоп)

alex55555 в сообщении #1377542 писал(а):

не приводит к появлению эффекта, а это и есть (по определению) признак ленивости

Ленивость с точки зрения семантики языка сводится к возможности создания самоссылающихся объектов и других объектов бесконечной вложенности. Если у вас в программе подобные вещи не используются, то вы никак не сможете отличить "ленивый" рантайм от "неленивого" по результату выполнения им вашей программы. (Только по потреблению памяти и времени работы, а это уже за пределами языковой семантики.) Соответственно, ввод-вывод и вообще побочные эффекты к этому никакого отношения не имеют.

[Munin]

warlock66613 в сообщении #1377602 писал(а):

Только по потреблению памяти и времени работы, а это уже за пределами языковой семантики.

Тонкий вопрос. Например, в C++ принято давать некоторые гарантии на уровне описания языка и библиотеки.

[arseniiv]

Если слишком заспецифицировать язык в этом отношении, может получиться, что нельзя использовать rewrite rules, а это очень важная вещь, с помощью которой например реализуется stream fusion, позволяющее не выделять память под временные списки, порождаемые и разбираемые определёнными функциями, которыми очень часто как раз и пользуются. Именно потому что они могут сильно менять такие параметры — время работы тоже. (Правда написанием своих таких правил можно сломать все гарантии и семантики тоже, но обычно используют их только в хорошо проработанных пакетах.) Потому иногда довольно непрозрачный вопрос, чему быть в спецификации, а чему быть в фольклоре.

[Legioner93]

warlock66613 в сообщении #1376832 писал(а):

Ещё (почти) пример "применения". Типы данных в Haskell образуют категорию $\operatorname{Hask}$, где морфизмами являются функции. На интуитивном уровне эта категория похожа на категорию множеств, и именно так она воспринимается при программировании. Но строго говоря это не категория множеств, и, наверное, теория категорий может cказать каково отношение между этими категориями, благодаря чему мы можем успешно считать типы Haskell множествами, а функции - функциями между множествами.

Кстати, Hask не является категорией, из-за наличия в языке seq и bottom нарушается свойство $f \circ id = f$

-- Пт фев 22, 2019 00:00:40 --

Munin в сообщении #1377616 писал(а):

Тонкий вопрос. Например, в C++ принято давать некоторые гарантии на уровне описания языка и библиотеки.

А можно пример того, о чём идёт речь?

[Munin]

Legioner93 в сообщении #1377641 писал(а):

А можно пример того, о чём идёт речь?

Ну например, время доступа в vector<> не более чем константа по числу членов, а время доступа в list<> не более чем линейно. Кажется, оверхед по памяти для POD не более чем линеен по полезному объёму, а оверхед за виртуальные методы - не более чем константа (если нет виртуальных базовых классов).

[warlock66613]

Legioner93, ну выкинуть seq (из рассмотрения). Я и без таких строгих аргументов чувствовал, что эта "функция" - грязный хак.

[alex55555]

(Оффтоп)

warlock66613 в сообщении #1377602 писал(а):

Ленивость с точки зрения семантики языка сводится к возможности создания самоссылающихся объектов и других объектов бесконечной вложенности.

Здесь вы как-то по своему определяете понятие ленивости. Что такое "самоссылающихся объектов"? Если это дерево, то там ссылки на аналогичный, но не идентичный объект. А если в буквальном смысле сам на себя, то зачем? Внутри объекта все поля и так доступны.

А вообще какое определение является "истинным" не знает никто, потому что по сути вот так исторически сложилось, что придумали call by need, который иногда выгоднее strict evaluation, которое в свою очередь определяют как:

Цитата:

In strict evaluation, the arguments to a function are always evaluated completely before the function is applied.

Соответственно, обратное к такому определению - не все аргументы вычисляются до вызова, либо не в полном объёме. Хотя в википедии пишут так:

Цитата:

delays the evaluation of an expression until its value is needed

Но когда оно там needed, вопрос остаётся открытым. Формально needed можно определить и как момент вызова функции, куда передаётся интересующий нас аргумент, тогда опять получаем strict. В общем-то обычная для абстрактных теорий ситуация - всё зависит от аксиом. Есть единые аксиомы в основе программирования? Подозреваю, что нет, ибо кто-ж их всем программирующим навяжет?

-- 22.02.2019, 13:31 --

(Оффтоп)

warlock66613 в сообщении #1377682 писал(а):

Я и без таких строгих аргументов чувствовал, что эта "функция" - грязный хак.

А как без хаков? Где-то должны быть эффекты. Всё чистым быть не может. Абстрактные теории должны как-то существовать в реальном мире.

-- 22.02.2019, 13:36 --

Legioner93 в сообщении #1377641 писал(а):

Кстати, Hask не является категорией, из-за наличия в языке seq и bottom нарушается свойство $f \circ id = f$

Авторы языка не рекомендуют рассматривать его составляющие с точки зрения теории категорий. В смысле они рекомендуют рассматривать всё просто как некие структуры данных и способы их обработки, без привлечения дополнительных абстракций. Но вот сами же описывают язык с привлечением понятий bottom и т.д.

Вообще успех хаскеля в математических кругах во многом обязан именно максимальной его близостью к математическим абстракциям, и при этом ещё и практической применимостью (в отличии от кучи эзотерических языков).