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

[rockclimber]

Кстати, а что такое "ленивое IO"?

[Anton_Peplov]

По разным затронутым вопросам.

Высшей математикой обычно называют всю ту математику, которую не изучают в школе (то есть $>99\%$ всей существующей математики). Разумеется, у тех, кто ей пользуется каждый день, нет никакой мотивации называть её высшей.

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

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

Джентльменский набор разделов математики, которые нужны во многих прикладных областях от физики до экономики - это матан, общая и линейная алгебра, ТФКП (включая Фурье-анализ), дифуры (обыкновенные и ДУЧП), теорвер/матстат. Возможно, ещё что-то забыл. Дальше уже меньше и чем дальше в абстрактные выси, тем меньше.

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

Базовый уровень по алгебре, она же высшая алгебра, она же абстрактная алгебра - уже упоминавшийся трёхтомник Кострикина. Весьма кстати он включает в себя и линейную алгебру.

В теории множеств можно остановиться на уровне "чем континуум отличается от счётного множества", а также прочитать про отношения эквивалентности и порядка и алгебру множеств. Всё это хорошо изложено в первой главе учебника Колмогорова и Фомина "Элементы теории функций и функционального анализа". Всё, что дальше, уже мало где применяется за пределами собственно теории множеств. Впрочем, на мой вкус, она сама по себе очень интересная наука, но я вообще люблю основания математики.

[warlock66613]

rockclimber в сообщении #1377030 писал(а):

Кстати, а что такое "ленивое IO"?

Допустим у нас есть большой файл со списком целых чисел и мы хотим хитрым образом преобразовать его в другой файл. И хотим мы это сделать в рамках pure-functional ЯП, например, Haskell.

Первый вариант, который приходит в голову, - прочитать весь файл, превратив его в список чисел в памяти, а затем позвать алгоритм преобразования, которые представлен чистой функцией (никакого IO, то есть никакой императивщины). Функция преобразования вернёт нам новый список, который мы затем запишем в результирующий файл. Итого у нас основная часть программы будет чистой функцией, а в IO-контексте мы будем только читать и записывать файлы. Одна проблема: файлы большие, и на самом деле для преобразования не требуется читать весь файл целиком.

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

Lazy I/O - это попытка разрешить эту дилемму с помощью очень хитрой функции hGetContents, которая превращает файл в как-бы-чистый список символов - то есть в строку (или в список байт, если бинарный файл). Хотя результирующая строка выглядит как обычная строка в памяти, на самом деле она "незаметно" читает символы из файла по мере необходимости.

Несмотря на определённую элегантность решения, результат ужасен:

The problem with lazy I/O писал(а):

For example, a common beginner mistake is to close a file before one has finished reading it:

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

wrong = do
    fileData <- withFile "test.txt" ReadMode hGetContents
    putStr fileData

The problem is withFile closes the handle before fileData is forced. The correct way is to pass all the code to withFile:

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

right = withFile "test.txt" ReadMode $ \handle -> do
    fileData <- hGetContents handle
    putStr fileData
 

Here, the data is consumed before withFile finishes.

Although this is easily fixed, the type system does not enforce the correct solution. Even worse, if you use the former code, it won't even raise an error – it will just fail silently and return an empty string. Many years passed before a satisfactory solution to the streaming data problem was found.

[rockclimber]

Anton_Peplov
warlock66613
Спасибо, пойду переваривать.

[alex55555]

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

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

обычное IO лениво в смысле выбора времени исполнения рантаймом

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

Вообще вот такой примерчик сляпал для демонстрации:

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

test :: Int -> Int
test x = putStr "xxx" `seq` 1
 

Если его вызывать в main, то будет выведена единица, а "ххх" не будет. А всё почему? Как я это понимаю, здесь вывод "ххх" не запускается из-за ленивости, ведь аргумент уходит в seq и там просто теряется. А неленивый язык бы сразу вычислил все входные параметры и, соответственно, выдал бы на экран "ххх", получили бы сторонний эффект в чистой функции. То есть ленивость всё же участвует в процессе.

Отсюда и разница между ленивым и неленивым IO становится менее очевидна.

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

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

Ну так машина Тьюринга "под капотом".

-- 19.02.2019, 17:35 --

Anton_Peplov в сообщении #1377032 писал(а):

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

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

(Оффтоп)

Anton_Peplov в сообщении #1377032 писал(а):

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

Интересно, а в чём интерес к "тому, что дальше"? Например бесконечности с их равенством мощностей мне совсем "не зашли" (сильно хочется опровергнуть такой подход).

[warlock66613]

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

здесь вывод "ххх" не запускается из-за ленивости

Нет, ленивость тут не при чём. Выражение putStr "xxx" имеет тип IO (), то есть RealWorld -> (RealWorld, ()). То есть это - функция. Чтобы произошёл вывод на экран, эту функцию надо позвать, передав в неё объект RealWorld. Вы же этого не делаете, а просто отдаёте seq эту невызванную функцию. В неленивом языке всё было бы абсолютно точно так же.

[alex55555]

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

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

здесь вывод "ххх" не запускается из-за ленивости

Нет, ленивость тут не при чём. Выражение putStr "xxx" имеет тип IO (), то есть RealWorld -> (RealWorld, ()). То есть это - функция. Чтобы произошёл вывод на экран, эту функцию надо позвать, передав в неё объект RealWorld. Вы же этого не делаете, а просто отдаёте seq эту невызванную функцию. В неленивом языке всё было бы абсолютно точно так же.

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

Да, ещё подумалось - само наличие такой возможности запоминания ссылки на незапущенное вычисление и есть следствие ленивости языка. Если бы лени не было, не было бы и запоминания незапущенного вычисления, поскольку оно бы сразу запускалось и далее передавался бы уже результат. А в данном случае передаётся не функция (у неё другой тип), а именно ссылка на вычисление. Хотя делается это неявно, а в очевидном (но неправильном) варианте передаётся объект типа IO.

[warlock66613]

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

IO всё же объект

В Хаскелле все функции - объекты, это не мешает им быть функциями. IO () - это функция.

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

На вход seq подаётся полностью готовая к исполнению конструкция, у неё нет отсутствующих параметров

У неё как раз есть именно что отсутствующий параметр (типа RealWorld).

-- 19.02.2019, 20:24 --

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

наличие такой возможности запоминания ссылки на незапущенное вычисление и есть следствие ленивости языка

Следствие ленивости языка - возможность делать это неявно. В неленивом языке (например, F#) соответствующая возможность так же присутствует, просто она требует её явного задействования. Но к монаде IO это всё отношения не имеет.

[arseniiv]

alex55555
Действие IO a выполнить «в обход main» невозможно*. Оно должно каким-то образом быть включено в то действие IO (), которое возвращает main, иначе оно останется, как уже писал warlock66613, «невостребованным», поскольку значений типа RealWorld нам никто не даёт: одно есть у рантайма, но он его применяет сам к тому, что дала main (и дальше уже будет какой-то спектакль). Ленивость тут позволяет просто не вычислять сразу всю махину-действие до его выполнения, а делать это по надобности. И всё.

* Ну могут быть конечно штучки с unsafePerformIO, но это отдельный разговор и вряд ли для этой темы.

[_Ivana]

alex55555, вы пишете глупости. О чем вам минимум 3 человека пытаются безуспешно намекнуть. Но, видимо, из-за лени вы не спешите форсить санки их посылов, продолжая генерировать свои. Может лучше заняться опровержением Кантора?

ЗЫ

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

Вообще на IO Хаскелла можно смотреть как на

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

[warlock66613]

_Ivana в сообщении #1377177 писал(а):

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

Так и есть. Кстати, может кому-нибудь будет интересно почитать: Как написать монаду IO на C# (не) без помощи параллельной вселенной и машины времени.

[alex55555]

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

В Хаскелле все функции - объекты, это не мешает им быть функциями.

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

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

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

На вход seq подаётся полностью готовая к исполнению конструкция, у неё нет отсутствующих параметров

У неё как раз есть именно что отсутствующий параметр (типа RealWorld).

Это "fake type". Если мы отдадим на вход любую другую функцию, например возвращающую Int, мы получим то же самое - она не выполнится. То есть RealWorld здесь ни при чём.

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

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

наличие такой возможности запоминания ссылки на незапущенное вычисление и есть следствие ленивости языка

Следствие ленивости языка - возможность делать это неявно. В неленивом языке (например, F#) соответствующая возможность так же присутствует, просто она требует её явного задействования. Но к монаде IO это всё отношения не имеет.

Да, в ленивом языке ленивость встроена, поэтому её нет нужды реализовывать самостоятельно, как придётся делать в любом неленивом языке. Но конкретно в хаскеле ленивость встроена и именно она позволяет отложить любые действия, в том числе IO. Без ленивости пришлось бы вручную рисовать необходимые враперы. Но вы ведь их не рисуете? Так как же тогда "ленивость отношения не имеет"?

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

Хотя в целом я не против утверждения о выборе времени выполнения IO рантаймом, но механизм ленивости в этом процессе явно присутствует.

-- 20.02.2019, 00:57 --

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

Действие IO a выполнить «в обход main» невозможно*. Оно должно каким-то образом быть включено в то действие IO (), которое возвращает main, иначе оно останется, как уже писал warlock66613, «невостребованным», поскольку значений типа RealWorld нам никто не даёт: одно есть у рантайма, но он его применяет сам к тому, что дала main (и дальше уже будет какой-то спектакль).

Вот давайте представим, что у нас в программе есть чтение из файла и на основе прочитанного вызов тех или иных функций. Теперь взглянем на ситуацию с объектом, который возвращает main. Что бы получить полное дерево обхода программы (ведь вы считаете, что без RealWorld выполнять вычисления нельзя) нам нужно сначала выяснить - а какую функцию выполнять. Но выяснить мы это можем лишь прочитав что-то из файла. Тогда получается, что из-за зависимости от RealWorld мы не сможем выполнить программу, ибо функция main не знает, а что собственно мы внутри неё будем вызывать. Можно предложить прочитать в память все доступные функции, но кроме того, что это неэффективно, это просто не поможет в случае наличия множества зависящих от входных данных путей исполнения. После некоторого размера дерева исполнения просто закончится память.

-- 20.02.2019, 01:04 --

_Ivana в сообщении #1377177 писал(а):

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

Вообще на IO Хаскелла можно смотреть как на

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

Ошибочное мнение. Например вот здесь приводят доказательства его некорректности.

[arseniiv]

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

Если мы отдадим на вход любую другую функцию, например возвращающую Int, мы получим то же самое - она не выполнится.

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

-- Ср фев 20, 2019 11:32:37 --

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

Но это не из-за лени

И это ведь должно быть ясно как день. Разумеется отсутствие лени никак не даст нам отсутствующие аргументы ex nihilo.

-- Ср фев 20, 2019 11:40:12 --

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

(ведь вы считаете, что без RealWorld выполнять вычисления нельзя)

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

-- Ср фев 20, 2019 11:44:13 --

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

После некоторого размера дерева исполнения просто закончится память.

Да, если бы рантайм сначала форсил main, а только потом выполнял полученное всё целиком действие, то под него в принципе* могло бы иногда не хватать памяти (но всё равно это не какое-то страшное препятствие). Это да. Но вы складываете в одну кучу то, что действительно есть, с тем, что не происходит, как в случае например объяснения работы putStrLn "1" `seq` 2.

* Что-то у меня подозрения насчёт частоты такого. Если вспомнить чем является >>=, кажется, зафорсить IO a «до конца», как вы подумали, вообще должно быть невозможно; сейчас проверю.

-- Ср фев 20, 2019 12:03:03 --

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

[alex55555]

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

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

Если мы отдадим на вход любую другую функцию, например возвращающую Int, мы получим то же самое - она не выполнится.

Потому что у неё нет аргумента, она не будет ни к чему применена.

Почему нет аргумента? С аргументом отдадим, что нам помешает?

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

Но это не из-за лени: всё же она зафорсится.

Что вы понимаете под словом "зафорсится"? Обычно это означает принудительное выполнение, то есть вариант без лени, но в дальнейшем тексте вы несколько по другому используете это слово.

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

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

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

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

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

(ведь вы считаете, что без RealWorld выполнять вычисления нельзя)

«Я считаю», что без него выполнить эффекты нельзя.

На чём основывается такое мнение? Даже теоретически - зачем нужен какой-то там фейковый объект, если у рантайма в распоряжении есть сам рантайм? Чего ему не хватит? У него и так всё есть.

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

если мы форсим значение типа IO a, мы после этого не выполняем эффект, который оно представляет.

Вот здесь непонятен смысл слова "форсим". Оно принуждает или? Невыполнение есть обратное к общепринятому смыслу слова to enforce.

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

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

В обычном понимании принуждения мы принуждаем рантайм выполнить любую операцию, которую считаем обязательной к мгновенному исполнению. Ну а эффекты при этом никак не фигурируют в описании принуждения, например в Haskell Report 2010. О принуждении говорится в контексте strict evaluation, то есть при исполнении без лени любой функции.

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

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

После некоторого размера дерева исполнения просто закончится память.

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

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

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

* Что-то у меня подозрения насчёт частоты такого. Если вспомнить чем является >>=, кажется, зафорсить IO a «до конца», как вы подумали, вообще должно быть невозможно; сейчас проверю.

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

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

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

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

[arseniiv]

(Оффтоп)

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

Почему нет аргумента? С аргументом отдадим, что нам помешает?

Ну а если есть, будет применена, да, просто вы написали «функцию», и проще было понять как просто голую функцию, а не применение её к чему-то.

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

Что вы понимаете под словом "зафорсится"? Обычно это означает принудительное выполнение, то есть вариант без лени, но в дальнейшем тексте вы несколько по другому используете это слово.

Принудительное вычисление, чтобы thunk превратился во что-то в слабой головной нормальной форме (WHNF).

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

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

Было, что можно проверить кодом (undefined :: IO ()) `seq` 1 — undefined вычислится и даст как полагается исключение. Я привёл его здесь к типу IO (), чтобы не возникало соблазна сказать, что IO a обрабатываются seq специальным образом.

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

На чём основывается такое мнение? Даже теоретически - зачем нужен какой-то там фейковый объект, если у рантайма в распоряжении есть сам рантайм? Чего ему не хватит? У него и так всё есть.

Как я уже написал, в подходе, использующем RealWorld, без него нельзя, по определению. В каком-то другом подходе можно обойтись без RealWorld вообще. Важно не это, важно что мы можем или не можем делать; сначала в этой теме решили показать, почему мы не можем делать что-то, взяв для иллюстрации этот подход. Но он не обязателен, просто если не лезть в реализацию IO, будет и нечем иллюстрировать вам, почему вы должны быть неправы. Можно, конечно, не пытаться ничего иллюстрировать, просто люди попались достаточно добрые.

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

Вот здесь непонятен смысл слова "форсим". Оно принуждает или?

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

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

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

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

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

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

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

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

Работ с эффектами скрыта в IO, которое, возможно, как-то по своему воспринимает необходимость исполнения.

Само по себе оно никак не воспринимает, в том и дело. Насколько я в курсе, никакой подход к функциональному вводу-выводу не использует изменений в стратегии вычисления именно для него.

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

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

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

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

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

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

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