?

Log in

No account? Create an account

[icon] /^.in$/
View:Recent Entries.
View:Archive.
View:Friends.
View:Profile.
View:Website (/me (домен, хотящийся в углу комнаты)).
Missed some entries? Then simply jump to the previous day or the next day.

Tags:, ,
Security:
Subject:Моноиды и прочие ужасы
Time:02:21 am
Не знаю откуда начать. В общем, в эту последнюю (уже сданную) сессию по «Языковым процессорам» было что-то типа домашнего задания, где был дан достаточно смешной язык программирования (операторы языка вписываются в двумерную матрицу, и переходы можно делать вверх-вниз-влево-вправо по всяким странным правилам) и нужно было по программе на этом языке построить Control-Flow граф и всячески его верифицировать, отвечая на вопросы типа «А может ли программа чисто теоретически завершиться?», «А может ли быть выход за пределы поля?», «А может ли быть чтение из переменной до записи в неё значения?» и тому подобных.
Не смотря на то, что реализовывать предлагалось на чём-то из списка [C++, C#, Java] я реализовал всё на Haskell, обильно комментируя весь код, чтобы его можно было понять даже не будучи знакомым с этим экзотерическим языком программирования. И, я думаю, мне это удалось.

Основная идея моего решения состояла в том, что на все задаваемые вопросы можно отвечать в терминах моноидов. Мне слишком лень тут устраивать какие-то туториалы по вездесущим моноидам и их использованию, и сегодня мне моё решение уже не кажется столь же умным, как казалось пару недель назад, и вообще пост не о том, как верифицировать Control-Flow графы с использованием моноидов. Просто скажу, что я вычленял из (направленного Control-Flow) графа некоторые деревья, для каждого узла дерева вычислял какое-то значение, а потом значения суммировал внутри каждого дерева и по всем деревьям.
Например, для ответа на вопрос «А может ли программа чисто теоретически завершиться?» для всех узлов графа без инструкции остановки это «какое-то» значение будет False, для узлов с инструкциями остановки — True, потом рассматриваем полученные элементы как моноид над булеанами с операцией дизъюнкции, суммируем, получаем ответ. Замечу также, что, поскольку там всё лениво вычисляется и суммируется, то этот способ не хуже, чем, например, поиск узлов с инструкцией остановки обходом в глубину с прерыванием обхода при первой найденной.

Вот теперь начинается интересное. В ответ на письмо со своей великой программой я, кроме всего прочего, получил вопрос «А есть ли вопросы о Control-Flow графе, на которые нельзя ответить с помощью моноидов?»
И вот в этом месте я задумался, и до сих пор не уверен, что правильно ответил на сей тонкий философский вопрос.

Во-первых, естественно, что _моя_ реализация не умела отвечать на вопросы, на которые не способна выдать «частичный ответ» (из которого получается «ответ» после суммирования с другими «частичными ответами») функция, вычисляющая «какое-то» значение для каждого узла графа (а на самом деле — дерева, как сказано выше). Но, если бы, например, эта функция рассматривала не только окрестность текущего узла, а вообще весь граф, то она, казалось бы, могла бы оказывать помощь в поиске ответа на куда более сложные вопросы.
Но сам тонкий философский вопрос поставлен так, что интересна верхняя грань сложности вопросов на которые вообще можно ответить суммируя элементы моноидов. Потому есть пункт «во-вторых».
Во-вторых, я, не смотря на то, что прекрасно понимаю, что почти ничего не понимаю в теории категорий (например, потому, что чтение «Категорий для работающего» вызывает у меня много проблем, связанных с тем, что нотация в этой книжке не проходит тайпчек в моей голове и очень много усилий уходит на поиск изоморфизмов, приводящих структуры, используемые автором, к понятному и корректному для моей головы виду), помню факт (который и без того «знает каждый младенец»), что «Монада есть моноид в категории её эндофункторов». Продолжая рассуждения на эту тему, я сделал заключение, что ответом на «А есть ли вопросы о Control-Flow графе, на которые нельзя ответить с помощью моноидов?» является «Нет», ибо если на какой-то вопрос можно ответить императивно (машиной Тьюринга), то можно упаковать это в монаду, а значит это что-то представимо в виде моноида. Я могу ошибаться.

Однако, не смотря на завораживающие подробности написанного выше, я хотел написать совсем не об этом. Просто ехал я тут в автобусе домой, рассуждал о стрелках, комонадах и зипперах в хаскеле, и подумалось мне «А чего ради это люди вообще засовывают достаточно простые вещи в зипперы и комонады, подводя под простой алгоритм кучу вроде бы не очень и нужной математики, а потом долго радуются, что у них оно почему-то работает?». И я стал прикидывать сколько времени я потратил раскладывая в моноиды ответы на вопросы по «Языковым процессорам», сколько времени строчил код, сколько времени дебажил (ненавижу хаскелевский Data.Array!!! почему нельзя хотя бы строчку в программе сказать, где оно падает?) и сколько времени дописывал к нему комментарии, и стал сравнивать со временем, которое на такое же задание потратил ivansorokin, писавший его на плюсах.
И надумалось мне, что если сделать скидку на мою общую тормознутость, то даже если у меня результирующего функционального кода в n раз меньше, чем получается на плюсах, то и пишу я его примерно в n раз медленнее. Не знаю, может быть я такой тормоз, потому что меняю язык программирования на новый раньше, чем успеваю привыкнуть к старому (сейчас на Agda облизываюсь, например), но мне показалось, что просто на самом деле нифига нет никакой разницы на чём писать, и эти постоянные холиворы на тему Плюсы-vs-Хаскель и etc — бред.
На мой взгляд, существенная разница только в способе рассуждений, ибо на плюсах я бы делал какой-нибудь обход в глубину, с прерыванием в случае, если на задаваемый вопрос уже можно однозначно ответить, а на хаскеле я родил функцию из содержимого узла в элемент моноида, реализовал Foldable для моего графа, а дальше нижележащая математика всё сделала сама. Хорошо это или плохо — думайте сами.
С другой стороны, для хаскелевского кода, я по крайней мере, знаю как формально доказать его корректность, а в плюсах с этим как-то очень плохо.

Кстати, о «модульности и расширяемости» каждого решения тоже можно поспорить, другое дело, что, наверное, если в плюсах задаться реализацией мегаобщего фреймворка для обхода и преобразования структур, то какой-нибудь Foldable с Traversable и получатся (только на стероидах и итераторах, небось), если уже чего-то подобного нет.
withComments $ arr (take 9) >>> delay new

[icon] /^.in$/
View:Recent Entries.
View:Archive.
View:Friends.
View:Profile.
View:Website (/me (домен, хотящийся в углу комнаты)).
Missed some entries? Then simply jump to the previous day or the next day.