Objective Caml - Понедельник, 2 апреля 2012

Objective Caml

ocaml@conference.jabber.ru

Понедельник, 2 апреля 2012< ^ >

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

[00:00:29] <Savik> хай
[00:00:45] <Savik> ребят, а верблюды как к арм относятся?
[00:01:26] <Kakadu> Savik: https://github.com/bmeurer/ocaml-arm
[00:06:03] komar вышел(а) из комнаты: Replaced by new connection
[00:06:04] komar вошёл(а) в комнату
[00:12:37] Savik вышел(а) из комнаты
[00:36:33] Kakadu вышел(а) из комнаты
[01:08:57] komar вышел(а) из комнаты
[01:10:59] komar вошёл(а) в комнату
[01:47:07] komar вышел(а) из комнаты
[01:48:17] komar вошёл(а) в комнату
[01:48:33] bobry вышел(а) из комнаты
[02:09:08] Typhon вошёл(а) в комнату
[02:34:54] komar вышел(а) из комнаты: Replaced by new connection
[02:34:54] komar вошёл(а) в комнату
[02:45:14] ftrvxmtrx вышел(а) из комнаты
[02:46:30] ftrvxmtrx вошёл(а) в комнату
[03:08:41] komar вышел(а) из комнаты
[03:10:33] komar вошёл(а) в комнату
[03:32:54] shaggie вышел(а) из комнаты
[03:36:54] letrec вошёл(а) в комнату
[03:42:55] Typhon вышел(а) из комнаты
[03:53:33] komar вышел(а) из комнаты
[03:53:38] komar вошёл(а) в комнату
[04:13:35] komar вышел(а) из комнаты
[04:14:28] komar вошёл(а) в комнату
[04:45:25] letrec вышел(а) из комнаты
[05:15:41] komar вышел(а) из комнаты
[05:16:24] komar вошёл(а) в комнату
[06:53:03] ermine вошёл(а) в комнату
[06:53:58] komar вышел(а) из комнаты: Replaced by new connection
[06:53:58] komar вошёл(а) в комнату
[07:40:28] komar вышел(а) из комнаты
[07:40:28] komar вошёл(а) в комнату
[07:49:23] Typhon вошёл(а) в комнату
[08:24:15] komar вышел(а) из комнаты
[08:26:19] komar вошёл(а) в комнату
[09:38:32] Typhon вышел(а) из комнаты
[09:58:23] komar вышел(а) из комнаты: Replaced by new connection
[09:58:23] komar вошёл(а) в комнату
[10:01:42] ftrvxmtrx вышел(а) из комнаты
[10:38:26] dzhon вошёл(а) в комнату
[10:39:55] <dzhon> Здравствуйте, уважаемые, а почему убрали сахар для парсеров из языка ([< 'p... >]) ? Что с этим делать и нужно ли вообще ? :)
[10:40:13] <komar> Ой.
[10:40:16] <komar> Я когда-то помнил и забыл.
[10:40:50] <komar> Оно то ли в camlp5 осталось...
[10:41:26] <komar> Короче, оно не нужно и пользуйся комбинаторами. Или той хренотой, которая у них сейчас тут модна, но на которой парсер написать невозможно.
[10:43:00] <gds> dzhon: через _tags допиши camlp4orf или какой-то из других camlp4-парсеров.  Их список можно получить через "ocamlbuild -documentation | grep camlp4", дальше методом тыка найдётся нужный.
[10:44:51] ftrvxmtrx вошёл(а) в комнату
[11:05:57] ftrvxmtrx вышел(а) из комнаты
[11:09:44] ftrvxmtrx вошёл(а) в комнату
[11:13:26] komar вышел(а) из комнаты
[11:16:19] komar вошёл(а) в комнату
[11:31:11] bobry вошёл(а) в комнату
[11:31:58] <bobry> dzhon: вроде ничего не убирали, как было в camlp4 так и осталось
[11:32:29] <dzhon> bobry: по книге O'Relly оно прям в языке должно было быть.
[11:32:54] <dzhon> Там даже нет пометки, что это extension %)
[11:32:55] <bobry> гм, оч странно, а что за книжка?
[11:33:05] <dzhon> http://caml.inria.fr/pub/docs/oreilly-book/html/book-ora040.html
[11:33:19] <bobry> Streams are an extension of the language, not part of the stable core of Objective CAML.
[11:33:23] <dzhon> а не, извиняюсь, помечено
[11:33:26] <dzhon> проглядел
[11:33:29] <bobry> == camlp4 extension
[11:51:19] komar вышел(а) из комнаты: Replaced by new connection
[11:51:19] komar вошёл(а) в комнату
[11:55:11] Sun][ вошёл(а) в комнату
[12:20:02] dzhon вышел(а) из комнаты: Replaced by new connection
[12:20:02] dzhon вошёл(а) в комнату
[12:30:13] <bobry> я понял в чем единственный бонус TH по сравнению с camlp4, он хотя бы документирован
[12:34:36] Kakadu вошёл(а) в комнату
[12:46:15] ftrvxmtrx вышел(а) из комнаты
[12:46:46] ftrvxmtrx вошёл(а) в комнату
[12:51:38] komar вышел(а) из комнаты: Replaced by new connection
[12:51:38] komar вошёл(а) в комнату
[12:52:45] shaggie вошёл(а) в комнату
[13:22:12] <Kakadu> Sun][: Ну как твои приключения с объективным верблюдом?
[13:23:11] <Sun][> Kakadu: потихоньку :) сейчас придумываю какую-нибудь небольшую интересную задачу для  того, что бы проверить полученные знания на практике
[13:24:58] <gds> Sun][: если будут известны какие-нибудь предпочитаемые "предметные области", чятик может что-нибудь и подскажет.
[13:25:51] <Sun][> gds: да фот фиг знает :), я пока склоняюсь к джаббер-ботику для чего-нибудь
[13:25:59] <Sun][> например для общения с твиттером, да =)
[13:26:10] <Kakadu> Sun][: а ты Qt как?
[13:26:25] <Kakadu> я вроде тебя спрашивал во вторник, но вроде и не тебя, не помню
[13:26:37] <Sun][> Kakadu: в связке с C++ - нормально, с остальным - пока никак :)
[13:27:05] <Sun][> Kakadu: меня меня :)
[13:28:03] <Kakadu> сосбтвенно я тут попиливал одну штуку, которая генерит код для соединялки окамля и кутэ
[13:28:18] <Kakadu> игрушечное приложение вроде работает
[13:29:20] <Kakadu> Sun][: хочешь поиграться?:
[13:29:43] <Sun][> Kakadu: давай попробую :)
[13:29:51] <Sun][> калькулятор напишу, например :)
[13:30:47] <Kakadu> ну попробуй вот это скомпилить сначала. без генератора. https://github.com/Kakadu/lablqt/tree/master/qml/test1
[13:31:30] <gds> Kakadu: а ты сам уже разобрался с qt?
[13:32:05] <Kakadu> gds: Ну я понял что с legacy возиться --- ничего полезного не выйдет, а вот Qt5 c его Qml --- вроде ОК
[13:32:21] <gds> то есть, qml у тебя работает?
[13:32:25] <Kakadu> gds: правда там больше чем генератора стабсов кодить нечего
[13:34:11] <Kakadu> gds: тестовый пример --- да. Нада потестить QML на чем-нибудь побольше. Проблема в том что я QML ни ухо ни рыло, и желания копаться сейчас нет. А с полпинка ничего не заводится, потому что  большинство примеров из инета требует какие-то библиотеки, некоторые из которых получаются только путём пересбора dev-версии кутэ5
[13:35:11] <gds> Kakadu: а, тогда одобряю расклад.  А то думал, что ты новенького натравил на неработающий код; это было бы негуманно.
[13:36:01] <Kakadu> Sun][: собственно идеально чтобы ты потестил QML + мой генератор, но для legacy тоже можно поиграться
[13:36:24] <Kakadu> Sun][: попробуй пока тестовый пример, потому будем компилять сам генератор
[13:37:11] <Kakadu> генератор вот: https://github.com/Kakadu/lablqt/tree/master/moc . Но для его компиляции надо доставить либы syck и ocaml-syck. в генте она есть в портажах, а в иной системе придется повозиться.
[13:38:40] <Kakadu> а мне к сожалению надо сбегать на пару.
[13:41:16] <Sun][> Удачи :)
[13:41:33] <Sun][> оно компилится и запускается, круто :)
[13:42:00] <Sun][> Kakadu: значит генератор дома буду тестить, тут у меня дебиан
[13:55:20] dzhon вышел(а) из комнаты: Replaced by new connection
[13:55:24] dzhon вошёл(а) в комнату
[13:58:51] komar вышел(а) из комнаты
[13:59:08] komar вошёл(а) в комнату
[14:20:31] Typhon вошёл(а) в комнату
[14:34:05] ftrvxmtrx вышел(а) из комнаты
[14:35:14] ftrvxmtrx вошёл(а) в комнату
[14:47:57] komar вышел(а) из комнаты
[14:50:15] komar вошёл(а) в комнату
[15:22:26] komar вышел(а) из комнаты
[15:26:27] <Kakadu> Sun][: ну у меня дома тоже дебиан. Я ставил из сорцов. А дома у тебя гента?
[15:26:57] <Sun][> Kakadu: угу, домак гента, на работе же генту нельзя :(
[15:28:19] <Kakadu> из сорцов не вариант? )
[15:30:03] dzhon вышел(а) из комнаты
[15:30:23] <Kakadu> в дебиане появилось: libyaml-syck-ocaml из unstable
[15:30:27] dzhon вошёл(а) в комнату
[15:30:29] <Kakadu> Sun][: ^^
[15:31:21] <Sun][> Kakadu: Да можно и из сырцов, просто на работе все же большую часть времени нужно работать, а не окамл изучать :)
[15:31:59] <Kakadu> bobry: скажи Sun][ что это не так)
[15:32:48] letrec вошёл(а) в комнату
[15:36:32] <bobry> Kakadu: ну я кстати работаю :)
[15:39:09] komar вошёл(а) в комнату
[15:45:37] Kakadu вышел(а) из комнаты
[15:45:40] Kakadu вошёл(а) в комнату
[16:08:58] <Kakadu> кстати, мы зарепортили баг с 3м оазисом?
[17:05:22] dzhon вышел(а) из комнаты: Replaced by new connection
[17:05:22] dzhon вошёл(а) в комнату
[17:14:35] bobry вышел(а) из комнаты
[17:48:45] ftrvxmtrx вышел(а) из комнаты
[18:39:21] komar вышел(а) из комнаты: Replaced by new connection
[18:39:22] komar вошёл(а) в комнату
[18:40:09] dzhon вышел(а) из комнаты: Replaced by new connection
[18:40:09] dzhon вошёл(а) в комнату
[18:45:28] Sun][ вышел(а) из комнаты
[18:58:01] Kakadu вышел(а) из комнаты
[19:04:10] ftrvxmtrx вошёл(а) в комнату
[19:06:13] ftrvxmtrx вышел(а) из комнаты
[19:08:52] ftrvxmtrx вошёл(а) в комнату
[19:11:48] komar вышел(а) из комнаты
[19:12:01] <gds> кто там хотел coq в окамле?  http://www.metaocaml.org/concoqtion/
[19:14:16] komar вошёл(а) в комнату
[19:17:36] <ermine> в камле или метакамле?
[19:19:03] <ermine> там вдобавок древность
[19:20:16] <ermine> gds: и где ты находишь такие залежалые вещи? на ирц? :)
[19:21:23] <gds> в секретных заначках!
[19:22:12] <ermine> замшелые заначки
[19:22:35] <gds> а сама как лихо закапываешь ссылки, любо-дорого поглядеть.
[19:22:37] ermine утром прочитала про доказательство 2+2=5 в coq, не понравилось
[19:24:44] <ermine> это же полная туфта, если можно вот так любую вещь объявить истиной, прикрываясь пустышкой
[19:25:53] <ermine> пустышка - это не только прибор для младенцев, а пустой тип, который имеет функция доказывающая, что любая вещь - истина
[19:26:01] Typhon вышел(а) из комнаты
[19:27:18] <gds> так там небось доказывают не "2+2=5", а то, что из какого-то ложного утверждения следует "2+2=5"?  В таком случае логично всё.  Не выводи следствий из ненаселённых типов и всё.  В рантайм это не просочится, так как значение ненаселённого типа ты просто не создашь.
[19:28:45] <gds> ну и вообще, поаккуратнее надо с аксиомами.  Как и в окамле с Obj, который, по сути, утверждает (если в терминах утверждений), что из данного утверждения следует любое другое.  Тот же стыд, только в рантайме.
[19:29:00] <ermine> gds: там говорилось, что unit - это истина по карри-говарду :)
[19:29:19] <gds> правильно говорится.  Простой пример -- изоморфизм 'a и unit -> 'a.
[19:29:43] <gds> соответствующие утверждениям A и True -> A.
[19:29:47] <ermine> а посему в юнит можно всё завернуть и плеваться
[19:30:07] <gds> в unit завернуть?  но как?
[19:32:16] <ermine> ну как Theorem it_is_true : forall x : A, 2+2=5., где A не имеет элементов
[19:32:41] dzhon вышел(а) из комнаты
[19:33:08] komar вышел(а) из комнаты
[19:34:18] <gds> в плане экстракции у тебя будет функция a -> ..., где значение типа "a" ты не сможешь создать, следовательно, не сможешь выполнить эту функцию.
А вот unit -- это другое, там не 0, а 1 значение.
[19:35:14] komar вошёл(а) в комнату
[19:37:56] <ermine> gds: а во что экстрактится Inductive A : Set := . ?
[19:37:57] <gds> то есть, из любого типа с 0 значениями можно вывести любое утверждение уникальным образом ("из лжи следует любое утверждение"), и из любого утверждения можно прийти к значению с одним конструктором, тоже уникальным образом ("если имеем какое-либо утверждение, всегда можем вернуть unit").
Вот тут уже проглядывает теория категорий с её инициальными и терминальными объектами.
[19:38:09] <gds> ermine: зависит от подробностей, обычно в sum type.
[19:38:51] <ermine> gds: а как в камле создать пустой sum?
[19:39:19] <ermine> такой A, оказывается, можно матчить как match a with end :)
[19:39:32] <ermine> в coq
[19:39:49] <ermine> короче, всё время полная лажа с костылями и косами вдоль дороги
[19:40:04] <gds> ermine: в revised syntax -- "type a = [];"
[19:40:54] <ermine> gds: а матч без бранчей тоже у вас существует?
[19:41:09] <gds> костылей в coq очень мало.  Пуристы считают костылём выделение отдельного Prop вдобавок к Set/Type, но это на любителя, тут есть и преимущества, и недостатки.  Остальное -- давай костыли, рассмотрим.
[19:42:10] <gds> ermine: ты не поверишь!
# type empt = [];
type empt = [  ]
# value f : empt -> 'a = fun em -> match em with [];
value f : empt -> 'a = <fun>
[19:42:29] <gds> надеюсь, к этому коду, в отличие от coq'овского, претензий нет? :]]
[19:43:30] gds бессердечно срывает покровы
[19:45:09] <ermine> к скобочкам есть!!!
[19:46:51] <gds> к синтаксису.  ок.  самые основательные претензии обычно предъявляют к синтаксису.
[19:47:29] ermine посмотрела в Camlp4 - похоже, действительно можно пустой матч сгенерить
[19:48:26] <ermine> gds: ну в отношении coq тоже примерно так
[19:48:54] <ermine> match e with end - звучит некузяво, равно как ":= ."
[19:49:23] letrec вышел(а) из комнаты
[19:50:10] <ermine> жалко что в tapl нет про зависимые типы
[19:50:28] <gds> ну хотя бы match там ограничен end'ом, в отличие от ocaml original syntax.
а := -- это нормально.  слишком часто рассматривается равенство, надо различать его от привязок.
[19:51:36] <ermine> gds: лерой - неудачник? (про синтаксис оригинала) :)
[19:52:15] Kakadu вошёл(а) в комнату
[19:52:46] Kakadu вышел(а) из комнаты
[19:54:07] <ermine> про деление функций на просто функции и рекурсивные в coq я уже плевалась, это видимо тяжкое наследие камла
[19:57:07] letrec вошёл(а) в комнату
[20:00:37] <gds> нет, там серьёзнее, чем в окамле.  Там для использования функции нужно доказать её завершимость (при индукции/fixpoint) или её продуктивность (при коиндукции/cofixpoint).  В полуприватной репке поищи "Function star" и дойди до неё в coq, погляди, что там и как.
[20:00:54] Kakadu вошёл(а) в комнату
[20:01:14] <ermine> Kakadu: присоединяйся к нашему обсуждению coq
[20:01:27] <Kakadu> ermine: я ни ухом ни рылом в коках
[20:02:01] <gds> да вообще, пока я мог проводить параллели с камлом, это было более-менее в топик.  А так -- навряд ли.  Можно, при желании, coq@cjr, штоле.
[20:03:02] <Kakadu> нада кнечно прокачаться
[20:03:07] <ermine> Kakadu:  http://adam.chlipala.net/cpdt/
[20:06:34] <gds> народ, вы уеврены, что coq вписывается в ocaml@cjr?  Я -- не очень.  ygrek наверное тоже не захочет всё это видеть, и я его пойму прекрасно.  То, что coq написан на окамле и умеет генерить в него -- это не повод, вроде бы.
[20:06:49] gds погулять на пару часиков
[20:08:33] <ermine> gds: а чем еще сертифицировать камловые проги?
[20:09:20] <ermine> да еще конфа в последнее время дохлая, надо же чем-то ее оживить, скалой, что ли
[20:10:54] <gds> камловое -- есть какие-то штуки, искать надо.  сходу "why" приходит на ум, но это вроде императивное.  а чтобы полное камло сертифицировать -- такого точно нет.
[20:12:42] <Kakadu> джень ли что-то ворганила для сертификации
[20:12:58] <ermine> gds: кстати, а само камло сертифицировано?
[20:13:13] <gds> ermine:  ет.
[20:14:56] <ermine> ну если ядро линукса уже пытались сертифицировать, то оно явно безопаснее и менее глючное, чем камло
[20:16:08] <ermine> Kakadu: а что это?
[20:29:17] <Kakadu> ermine: я не помню
[20:53:31] shaggie вышел(а) из комнаты
[21:03:13] letrec вышел(а) из комнаты
[21:30:29] komar вышел(а) из комнаты: Replaced by new connection
[21:30:30] komar вошёл(а) в комнату
[21:59:34] ftrvxmtrx вышел(а) из комнаты
[22:10:01] bobry вошёл(а) в комнату
[22:44:23] ftrvxmtrx вошёл(а) в комнату
[22:50:12] ermine вышел(а) из комнаты
[23:22:25] <Kakadu> магический этот ваш кок
[23:26:25] <gds> Kakadu: по крайней мере в двух смыслах -- да.
[23:27:22] <Kakadu> немного на него посмотрел. Может выложить на гитхаб свю курсовую про доказательство предикатов.... Авось какому-то студенту понадобится
[23:28:09] <gds> предикаты -- first order logic?  мало кому.
[23:59:59] Typhon вошёл(а) в комнату