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

[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

[zeit-raffer.livejournal.com]

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

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

[nponeccop.livejournal.com]

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

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

[zeit-raffer.livejournal.com]

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