срезал как у бунина

[juan_gandhi]

PavelVelikhov 2 марта 2015 в 07:55
И еще в догонку — дайте пожалуйста формальное определение монады в формализме ZFC а не в теории категорий.

vpatryshev 2 марта 2015 в 09:29

Ну все, Глеб срезал.

ZFC ваше тут ни пришей не пристегни, товарищ оппонент. Монады от теории множеств не зависят.

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

PavelVelikhov 2 марта 2015 в 09:46
О да, срезал, как у Бунина… ZFC со всеми объектами нормально работает, видимо вы не в курсе.

http://habrahabr.ru/post/251747/

Comments

[nponeccop.livejournal.com]

Ну это ж известная вещь. Боттом гадит, с ним пропадает алгебраичность. Он бы ещё удивился некоммутативности or или нарушению x or true = true

Даёшь тотальные языки с санками!

[zeit-raffer.livejournal.com]

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

А зачем тотальным санки, чтобы тотальные и ленивые одновременно? Как-то это странно звучит.

[nponeccop.livejournal.com]

> А зачем тотальным санки

Некоторые термы меньше памяти едят в процессе CBN-редукции, чем СBV. А так это известный бред, что тотальным санки не нужны. Типа давайте раз порядок редукций не важен, лепить все СBV. Он-то неважен, но только с точки зрения терминируемости (будет терминироваться при любом раскладе). А так вам будет очень неприятно, например, если в ифе будут обе ветви вычисляться, пусть даже при этом зацикливания происходить не будет. Пример - бинарный поиск. Проход всех ветвей тотален, но с точки зрения ресурсов не имеет смысла.

[zeit-raffer.livejournal.com]

Всё-всё, уже осознал и исправился.
Попутно осознал, что Агда компилируется в Хаскель именно с ленивыми вызовами. В отличие от Идриса, например, который таки дефолтно строгий. Из-за чего If там имеет вполне ожидаемый тип
(b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a

[juan-gandhi.livejournal.com]

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

А... в Хаскеле это как раз все одно, что боттом...

[nponeccop.livejournal.com]

Ну да, отсутствие деления на индукцию и коиндукцию это другая сторона той же медали

[nponeccop.livejournal.com]

> в Хаскеле это как раз все одно, что боттом...

не, не всё равно. Определяете instance Num Peano и вперёд, я даже по этому поводу на SO спрашивал

http://stackoverflow.com/q/8474488

Если точнее, проблема не в бесконечных списках, а в отсутствии чисто индуктивных типов, т.е. в отсутствии деления на индуктивные и коиндуктивные типы, как я понимаю.

[juan-gandhi.livejournal.com]

О ни фига себе, этого я не знал.

А зачем это все нужно? Или исключительно для ленивости, и потому что termination...
Вот же ж блин.

[nponeccop.livejournal.com]

Я думаю, что это получилось само собой. Ну и если рассматривать term graph rewriting systems как семантику хаскеля с паттерн-матчингом (в ЛИ нет паттернов), то там это тоже получается само собой.