Objective Caml - Вторник, 3 апреля 2012

Objective Caml

ocaml@conference.jabber.ru

Вторник, 3 апреля 2012< ^ >

Конфигурация комнаты

[00:13:50] <bobry> бесполезней представления графа наверное нельзя придумать
[00:14:08] <bobry> все делает чтобы показать что функциональщина "ни на что не годится в real world"
[00:14:16] <bobry> даже не vertex -> vertex list
[00:14:27] <bobry> а type graph = size * vertex -> vertex -> bool
[00:14:54] <bobry> второй элемент пары должен быть в скобках
[00:17:05] <gds> вот за подобную х-ню (в обоих смыслах) я ненавижу функциональное программирование.
[00:18:04] <bobry> ну да, он еще сет предлагает функциями кодировать
[00:18:08] <bobry> причем на полном серьезе
[00:18:11] <bobry> уже 3 лекции
[00:18:15] <bobry> *facepalm*
[00:18:30] <bobry> вроде поигрались и хватит, расскажи как правильно та, но нет
[00:18:51] <gds> а у него ноги в рот помещаются?  Рекомендую проверить.
[00:20:17] <bobry> :D
[00:20:17] <gds> таких игрунов, игрунчиков, ну просто шалунишек эдаких праативненьких -- полным полно среди функциональщиков.
[00:20:33] <bobry> так это йома взрослый мужык который фул тайм на жаве пишет
[00:20:38] <bobry> что спрашивается за детский сад
[00:20:50] <gds> а.  жаба.  объясняет.
[00:21:21] <gds> цитирую говно:
"
Is there a good reason why there is no Pair in Java?
>In this  thread on comp.lang.java.help, Hunter Gratzner gives some arguments  against the presence of a Pair construct in Java. The main argument is  that a class Pair doesn't convey any semantics about the relationship  between the two values (how do you know what "first" and "second" mean  ?).
"
[00:22:03] <gds> via lj\jakobz
[00:23:02] <bobry> fuckye
[00:23:05] <bobry> даже в плюсах есть
[00:23:41] <gds> да херня про собственно pair, меня аргументация убила вусмерть.
[00:25:47] <gds> в общем, функциональщину дискредитируют эти преподы.
[00:51:50] <Typhon> > даже в плюсах есть
[00:52:14] <Typhon> помогал тут студенткам, так им преподаватель сказал, что вместо pair надо свой класс городить :)
[00:52:27] <bobry> побольше преподов таких!
[00:53:06] <Typhon> чтобы на ц++ писать не хотелось?
[01:20:23] komar вышел(а) из комнаты: Replaced by new connection
[01:20:24] komar вошёл(а) в комнату
[01:26:33] Kakadu вышел(а) из комнаты
[01:32:17] gds вышел(а) из комнаты
[02:06:06] bobry вышел(а) из комнаты
[02:10:17] komar вышел(а) из комнаты
[02:10:23] komar вошёл(а) в комнату
[03:21:13] komar вышел(а) из комнаты
[03:21:31] komar вошёл(а) в комнату
[03:26:54] Typhon вышел(а) из комнаты
[04:58:25] komar вышел(а) из комнаты: Replaced by new connection
[04:58:25] komar вошёл(а) в комнату
[05:29:26] komar вышел(а) из комнаты: Replaced by new connection
[05:29:27] komar вошёл(а) в комнату
[06:02:30] komar вышел(а) из комнаты
[06:06:01] komar вошёл(а) в комнату
[09:59:42] bobry вошёл(а) в комнату
[10:21:18] bobry вышел(а) из комнаты
[10:21:49] ftrvxmtrx вышел(а) из комнаты
[11:05:13] ftrvxmtrx вошёл(а) в комнату
[11:08:14] gds вошёл(а) в комнату
[11:41:18] bobry вошёл(а) в комнату
[12:14:58] Kakadu вошёл(а) в комнату
[12:35:50] ermine вошёл(а) в комнату
[13:04:49] bobry вышел(а) из комнаты
[13:07:28] bobry вошёл(а) в комнату
[13:15:22] ftrvxmtrx вышел(а) из комнаты
[13:28:14] shaggie вошёл(а) в комнату
[13:43:30] ftrvxmtrx вошёл(а) в комнату
[13:49:33] Typhon вошёл(а) в комнату
[13:50:27] ftrvxmtrx вышел(а) из комнаты
[13:52:19] komar вышел(а) из комнаты: Replaced by new connection
[13:52:20] komar вошёл(а) в комнату
[14:02:06] ftrvxmtrx вошёл(а) в комнату
[14:06:40] ftrvxmtrx вышел(а) из комнаты
[14:09:41] ftrvxmtrx вошёл(а) в комнату
[14:35:00] Typhon вышел(а) из комнаты: Replaced by new connection
[14:35:32] Typhon вошёл(а) в комнату
[15:29:35] <Kakadu> слушайте, так Кок ничего сам не доказывавет, нада по мере написания функций их доказывать?
[15:37:34] <gds> если ты действительно хочешь что-то доказать -- надо доказывать.  Если не хочешь -- пиши как есть, считай, что это такой ML, только с более мощными типами.
Но для рекурсий/корекурсий надо будет доказать соответственно завершимость либо продуктивность.
Однако есть хаки, позволяющие использовать в коде недоказанные рекурсивные функции.
[15:38:19] <Kakadu> какой-то нелаконичный ML в первом приближении
[15:39:04] ftrvxmtrx вышел(а) из комнаты
[15:40:50] <gds> многоцелевая штука, как для программирования, так и для доказательств, и везде нужно, чтобы был ясен контекст, в котором находится данный кусок исходника.  И, конечно, такие вещи, как полиморфные варианты и объекты в coq отсутствуют (хотя и эмулируются; уже понял, как).
[16:22:16] <ermine> Kakadu: а ты ждал чуда от коки?
[16:22:27] <Kakadu> да
[16:23:28] <ermine> а у него в названии есть слово assistant, а от ассистентов чуда обычно не ждут
[16:27:00] <Kakadu> вот такая вот эизнь гавно
[16:27:05] <Kakadu> жизнь*
[16:56:47] klapaucius вышел(а) из комнаты
[17:17:16] klapaucius вошёл(а) в комнату
[17:51:05] klapaucius вышел(а) из комнаты
[18:18:21] <gds> Kakadu: твоя -- вероятно :]
С другой стороны, есть кое-что про верификацию ml-кода, но настолько ненужно, что проще надёжный код сразу в coq писать, а остальную программу -- на окамле, например.  Всё будет работать совместно.
[18:27:36] <gds> Kakadu: но учти, что есть ещё http://coq.inria.fr/related-tools , может что понравится, но навряд ли.
[18:35:19] letrec вошёл(а) в комнату
[18:39:55] <bobry> мда, TH это какой то ад
[18:40:07] <gds> Kakadu: кстати, есть ещё http://coq.inria.fr/distrib/V8.3pl4/refman/Reference-Manual028.html , там оно пытается кое-что доказать само, где может.
[18:40:13] <gds> bobry: ну дык!
[18:40:43] <bobry> особено после camlp4, все там через жо со своей манаткой Q
[18:43:04] <gds> зато документация!
[18:43:22] <gds> ну и понт, конечно.
[18:43:24] <gds> TH ведь.
[18:43:42] <bobry> про документацию я похоже соврал — максимум API docs + посты
[18:43:50] <bobry> хотя у camlp4 и с API туговато
[18:44:00] <gds> хотя вот, для меня "TH" расшифровывается до сих пор как "TechHelp"/"THelp!", была такая штука давно.
[18:44:11] <bobry> :)
[19:24:10] bobry вышел(а) из комнаты
[19:25:10] Kakadu вышел(а) из комнаты
[20:17:54] Kakadu вошёл(а) в комнату
[20:37:47] ftrvxmtrx вошёл(а) в комнату
[20:54:30] letrec вышел(а) из комнаты
[20:58:15] bobry вошёл(а) в комнату
[21:55:50] shaggie вышел(а) из комнаты
[22:15:05] Typhon вышел(а) из комнаты
[22:44:30] <bobry> https://www.coursera.org/course/compilers
[22:44:32] <bobry> C++!
[22:44:44] <bobry> напиши свой компелятор на плюсах, вот это шутники
[23:23:25] <gds> в том числе про камломодули: http://diam-2003.livejournal.com/526682.html
[23:27:34] ermine вышел(а) из комнаты
[23:37:05] Typhon вошёл(а) в комнату