Objective Caml - Среда, 22 мая 2013

Objective Caml

ocaml@conference.jabber.ru

Среда, 22 мая 2013< ^ >

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

Участники комнаты

GMT+4
[01:10:09] tilarids вошёл(а) в комнату
[01:28:53] Kakadu вышел(а) из комнаты
[01:51:50] Zbroyar вошёл(а) в комнату
[03:37:10] tilarids вышел(а) из комнаты: Machine going to sleep
[05:16:50] zinid вошёл(а) в комнату
[06:58:09] avkarpich вошёл(а) в комнату
[07:57:02] f[x] вошёл(а) в комнату
[08:10:36] tilarids вошёл(а) в комнату
[08:14:14] f[x] зашкварился : https://github.com/OCamlPro/opam-repository/pull/729
[08:44:31] tilarids вышел(а) из комнаты: Machine going to sleep
[09:48:51] f[x] вышел(а) из комнаты
[09:58:14] ftrvxmtrx вышел(а) из комнаты
[10:49:42] komar вышел(а) из комнаты: Logged out
[11:25:44] <avkarpich> Посоны, а есть ли какой-нибудь coding style guide а-ля pep8 для coq? Нашел только вот это небольшое описание http://coq.inria.fr/cocorico/CoqStyle#Variables_inside_proofs
[11:28:04] komar вошёл(а) в комнату
[11:29:20] f[x] вошёл(а) в комнату
[11:30:51] <f[x]> coding style нужен когда над кодом несколько человек работает
[11:32:21] <avkarpich> т.е. общепринятого стандарта нет?
[11:33:52] <f[x]> я на коке не сижу, но подозреваю что нет, т.к. обычно доказательства пишутся одним человеком
[11:34:10] <f[x]> надо смотреть как пишут "иконы стиля" и копировать у них :)
[11:34:43] <f[x]> из местных кокаинистов gds может что-то сказать
[11:35:25] <avkarpich> ок, подожду пока gds скастуется.
[11:38:24] Kakadu вошёл(а) в комнату
[11:51:50] ermine вошёл(а) в комнату
[13:52:35] ftrvxmtrx вошёл(а) в комнату
[14:32:04] Zbroyar вышел(а) из комнаты
[14:51:47] klapaucius вышел(а) из комнаты
[15:05:59] avkarpich вышел(а) из комнаты
[15:21:28] komar вышел(а) из комнаты
[15:35:12] f[x] вышел(а) из комнаты
[15:42:22] komar вошёл(а) в комнату
[15:43:33] komar вышел(а) из комнаты
[15:43:37] komar вошёл(а) в комнату
[15:51:41] ftrvxmtrx вышел(а) из комнаты
[15:52:22] ftrvxmtrx вошёл(а) в комнату
[15:59:24] <gds> f[x]: а я как раз хотел намекнуть тебе про extlib, чтобы ты её туда.
[16:03:04] <gds> avkarpich: про стиль в coq -- как-то в #coq irc поднимали вопрос, ответ был идентичен ответу f[x].  Я бы использовал здравый смысл тут.  Код должен быть понятным и приятным для чтения, доказательства -- желательно максимально автоматизированными, где это возможно, или хотя бы понятными при беганьи по ним через какой-нибудь coqide.
[16:11:22] Kakadu вышел(а) из комнаты
[16:12:51] Kakadu вошёл(а) в комнату
[17:10:51] tilarids вошёл(а) в комнату
[17:19:45] <gds> Kakadu: ты как-то поднимал вопрос про "in-memory database".  У меня похожая нужда возникла.  Что-то типа "есть структуры данных, есть определённые связи между ними, и нужно поддерживать 2..3 хештаблицы, чтобы обеспечить быстрый поиск одних данных по другим и наоборот".  В общем, надо бы продумать, как достаточно общо описывать взаимосвязи между данными, и надрочить тупую кодогенерилку, которая делала бы функции типа "get_x_by_y : x -> y", "store_x_y : x -> y -> unit", чтобы они работали на нескольких хештаблицах/деревьях/списках одновременно.
[17:20:09] zinid вышел(а) из комнаты
[17:23:40] <komar> > get_x_by_y
[17:24:16] <komar> Из этой херни рельсы наполовину состоят. Не-не, не. Разве что в целях оптимизации, тогда можно.
[17:25:39] <Kakadu> Да, надо подумать
[17:39:59] <Kakadu> вот только мне не совсем понятно что такое икс и игрек, потому что у меня с течением времени могли появляться новые
[18:25:00] <gds> komar: ну надо же как-то назвать функции, делающие внутри что-то типа Hashtbl.find h k.  Ну, можно x_of_y.
[18:26:08] <gds> Kakadu: x, y -- наименования сущностей.  Конечно, появляются и другие, оттуда и желание кодогенерить, чтобы компилятор указал, где и что надо поменять при изменении сущностей.
[18:27:43] komar вышел(а) из комнаты: Logged out
[18:42:26] <Kakadu> gds: у меня во время работы появляются, а не во время компиляции
[18:42:59] <gds> а, значит неактуально тебе оно.
динамическую типизацию бери, гыгы
[19:16:24] ermine страдает, что в камле match .. with фигово матчит
[19:17:22] <ermine> алгебраические типы существуют потому что match фигово матчит и норовит создать новые переменные
[19:17:49] <ermine> например let text = "abc" in match v with | text -> ...
[19:18:58] <ermine> а у меня тут тупняк как "неизвестное" превратить в алгебраику, стоит ли загрязнять алгебраику левыми сущностями, чтобы можно было матчить
[19:23:09] <gds> ermine: опиши подробнее, что делаешь.
[19:25:45] <ermine> gds: маплю из хмля в структуру, надо обработать "нестандартный случа", а эта обработка обычно решается либо экспшном, либо мусорным вариантом в алгебраических типах. Экспшн не хочется, а матчить структуру надо при дальнейшей работе с ней
[19:26:28] <ermine> вносить нестандартный вариант не хочется, чтобы не было грязи
[19:29:37] <ermine> gds: вот пример, ты знаешь, что тебе на вход поступят "а", "б" или "с", делаешь соответственно тип type t = | A | B | C и весело клепаешь string_of, of_string функции
[19:30:38] <ermine> gds: ну что ты делаешь в случае, если приходит "о"? Игнорировать? Бросать экспшн? добавить левый тип?
[19:34:12] <gds> ermine: а что с этим левым значением дальше будет сделано?  Если оно является признаком ошибки, то исключение бросать.  Если таки надо обработать -- | Other of ...
[19:35:29] ftrvxmtrx вышел(а) из комнаты
[19:39:11] <ermine> gds: а вот хочу матчить, а не конвертить в костыльные типы
[19:47:16] komar вошёл(а) в комнату
[20:32:36] f[x] вошёл(а) в комнату
[20:42:12] Kakadu вышел(а) из комнаты
[21:44:57] Kakadu вошёл(а) в комнату
[21:54:09] tilarids вышел(а) из комнаты: Computer went to sleep
[21:58:13] tilarids вошёл(а) в комнату
[21:58:20] tilarids вышел(а) из комнаты: Computer went to sleep
[22:06:33] f[x] вышел(а) из комнаты
[22:46:09] tilarids вошёл(а) в комнату
[22:56:41] komar вышел(а) из комнаты
[22:59:37] ermine вышел(а) из комнаты
[23:02:20] ftrvxmtrx вошёл(а) в комнату
[23:52:21] komar вошёл(а) в комнату