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

[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

[1master.livejournal.com]

Ну если на хабр ходить, то чего удивляться то.

[juan-gandhi.livejournal.com]

Да Царев спровоцировал; он везде успевает (и по бабам тоже).

[iz-chicago.livejournal.com]

У Шукшина?

[juan-gandhi.livejournal.com]

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

[yatur.livejournal.com]

Я так понимаю, имелся в виду расказ Шукшина "Срезал"?

[juan-gandhi.livejournal.com]

Ну имелся, конечно. Типичный же случай.

[andybil.livejournal.com]

Хабра-швабра

[zeit-raffer.livejournal.com]

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

[andybil.livejournal.com]

Занести, видимо, как везде России.
Или написать статью в песочницу, и ждать, вдуг кто даст инвайт.
Но за один непонравившийся коммент вам сольют карму и тогда вы снова ничего не сможете комментировать.
Это общество агрессивных садистов. Воспитание в стиле таракана, что бы не смели высовываться. В последнее время аудитория падает, а больше площадок на русском нет, кроме ЖЖ, здесь рот затыкает только хозяин ЖЖ, а там - толпа расстреливает. Остался один копипаст.

[zeit-raffer.livejournal.com]

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

[andybil.livejournal.com]

Это не глупая игра, это массовое воспитание привычки подавлять инакомыслие толпой. Крымнаш, например

[zeit-raffer.livejournal.com]

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

[juan-gandhi.livejournal.com]

У меня были те же проблемы, годами. Потом вдруг бац - и впустили в свой мордор.

[triampurum.livejournal.com]

> Хабра-швабра

Напомнили про лучший пост на этом вашем/их хабре, http://habrahabr.ru/company/mosigra/blog/251465/

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

Сложный интерфейс

[andybil.livejournal.com]

Ну-ка представьте, вас закинули на планету в Андромеде без штанов. Определить размер планеты и календарь. Я на вас посмотрю, как вы найдёте, что 12 месяцев, один год, неделя и т.п. Тем более, что звезда вращается вокруг планеты, а стоит планета на трёх (!?) слонах.

Re: Сложный интерфейс

[juan-gandhi.livejournal.com]

Ой люблю такие каменты!

Re: Сложный интерфейс

[triampurum.livejournal.com]

яннп

Re: Сложный интерфейс

[andybil.livejournal.com]

});

Re: Сложный интерфейс

[triampurum.livejournal.com]

еправда.

Re: Сложный интерфейс

[andybil.livejournal.com]

Специально для вас http://elementy.ru/lib/432522

[thedeemon.livejournal.com]

Понавучаца монадам и калькулюсам, а потом бах, и в хаскеле списки не свободные моноиды.

[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 как семантику хаскеля с паттерн-матчингом (в ЛИ нет паттернов), то там это тоже получается само собой.

[zeit-raffer.livejournal.com]

Ну, во-первых, ZFC тут и вовсе беспомощна, надо было спрашивать хотя бы про NBG.
Во-вторых, можно этот философический вопрос озвучить совсем без ТК:
транзисторы, которые в процессоре, когда выполняют код какой-нибудь фабрики синглетонов, работают как транзисторы или как фабрика синглетонов? И, если мы согласимся, что именно как транзисторы, то не следует ли отсюда, что программисту паттерны ООП "нинужны", а достаточно инженерной подготовки, чтобы рисовать схемы с этими транзисторами?

[nponeccop.livejournal.com]

А почему она беспомощна? Неконструктивность или с размерами проблема? Если второе то можно в малых категориях определить, не?

[zeit-raffer.livejournal.com]

Да, в малых можно. Но хочется же (и практически требуется) в больших!

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

[nponeccop.livejournal.com]

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

Можно ещё в MLTT ему предложить, может, устроит.

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

Вам надо было просто признаться, что ZFC вы не владеете за ненадобностью, и нагуглить товарищу ссылок. DH0 name calling имхо неуместен (но мне лень лезть в гадюшни хабра смотреть, что же произошло, так что take it with a grain of salt)

А так да - отечественное образование сильно перекошено в сторону числовых рассчётов и обобщений R, что в технических вузах, что в матмехах (у меня впрочем по матмехам выборка из одной харьковской точки). Алгебра и логика не то чтобы не в почёте, но центрального значения не придают и в техвузах не преподают вовсе, как впрочем и ZFC.

[migmit.livejournal.com]

В принципе, да, можно, но человек, кидающийся словами типа ZFC и не знающий ТК выглядит как-то очень странно.

[zeit-raffer.livejournal.com]

> что ZFC вы не владеете за ненадобностью

Отчего Вы уверены, что автор этого блога таки не владеет ZFC? :)
По крайней мере в том объёме, чтоб оттранслировать определение монады.

[juan-gandhi.livejournal.com]

Автор этого блога эту зиэфси преподает как бы.
Не припомню, какая из аксиом, кроме, может быть, аксиомы пар и аксиомы выделения, вообще имеют отношение к определению пары функций, необходимых для монады. С таким же успехом можно было просить определить монаду на моноиде Z₂.

Впрочем, интересные упражнения.

[norian.livejournal.com]

обычная "дискуссия" уровня подворотни

- слышь, чувачок, крутани тройное сальто нам на потеху
чо, не можешь ? ну ты лооох ..

[zeit-raffer.livejournal.com]

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

Зато собирать такие заблуждения интересно. С точки зрения того, чтобы знать, с какими заблуждениями придется столкнуться в будущем (предполагая, что заблуждения повторяются). Например, наш пациент, с одной стороны, упомянул в своем обзоре функциональные языки (Scala, Haskell), но именно как языки. Стоящей за ними огромной теории, без знания которой трудно называть человека знающим тот же computer science, он не только не заметил в обзоре, но и отмежевывается от нее в комментариях. Это же прекрасный парадокс!

[nponeccop.livejournal.com]

Нда, хорошо что я ссылку так и не открыл.

[juan-gandhi.livejournal.com]

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

[ionial.livejournal.com]

А есть слайды?

[juan-gandhi.livejournal.com]

Я матрицы в слайды еще не вставил; в следующий раз уже. Недавно дошло.

Сегодня как раз впаривал - шло замечательно. Даже Setf как категорию впендюрил в виде матриц, как вариант.

[belezbar.livejournal.com]

Почему-то автор поспешил записать вас в "агрессивные хаскелисты". На хабре вообще ФП не особо жалуют, по моим наблюдениям, однобоко как-то всё. Ну флаг им в руки. А что до статьи, так вот здесь http://sharpc.livejournal.com/67583.html, наверное, полнее. Даже автомат Калашникова есть.

[yussouf.livejournal.com]

это что - троллинг такой, по ссылке у вас?

не могу поверить, что ЭТО можно серьезно нести

[belezbar.livejournal.com]

Можно уточнить, что "ЭТО"? Вы про содержимое статей? По мне, так обе они вполне себе бесполезны, для меня, по крайней мере. На практике мне, максимум, с чем приходится иметь дело - реляционная алгебра в случае каких-нибудь хитрых SQL запросов. Остальное всё давно в библиотеках/фреймворках, гитхаб вон по швам трещит. Так что, соглашусь, что серьёзно нести это не стоит.

[yussouf.livejournal.com]

да все

но начать (и закончить, тут же) можно с предложения, на голубом глазу, начать теорминимум со штудий стандарта цпп

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

[udpn.livejournal.com]

А чем теоретический минимум плох?

[yussouf.livejournal.com]

первій текст, что ли?

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

то вам не треба, а это мы ваще отметаем как буржуазное...

у товарища, как-то, похоже, нет такого осчусчения, что опыт в этом мире бывает не только его собственный

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

и ссылки полезные есть

[udpn.livejournal.com]

Нет, я про http://sharpc.livejournal.com/67583.html

[yussouf.livejournal.com]

да я не стал даже особо вчитываться дальше - sapienti sat

но крайнюю шизофазоидность сего высе текста вынужден был отметить даже аффтар, ггг

[udpn.livejournal.com]

Вы, должно быть, про свои комментарии? :)

[yussouf.livejournal.com]

(терпеливо, участливо)

вы скажите какая часть вам непонятна - я, быть может, поясню

[juan-gandhi.livejournal.com]

Речи прямо как у кота, которому хорошо быть кисою, хорошо и собакою.

[belezbar.livejournal.com]

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

[juan-gandhi.livejournal.com]

Да у всех эта дилемма.

[http://users.livejournal.com/_xacid_/]

я статейку эту даже читать не стал - хватило названия.

[si14.livejournal.com]

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

Как крестьяне с электричеством, право слово. «Электристы».