Objective Caml - Четверг, 28 марта 2013

Objective Caml

ocaml@conference.jabber.ru

Четверг, 28 марта 2013< ^ >

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

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

GMT+4
[00:23:08] UncleVasya вышел(а) из комнаты
[00:24:13] f[x] вышел(а) из комнаты
[00:27:36] Typhon вышел(а) из комнаты
[00:58:45] Sun][ вышел(а) из комнаты
[01:01:43] Kakadu вышел(а) из комнаты
[01:53:03] f[x] вошёл(а) в комнату
[02:08:07] f[x] вышел(а) из комнаты
[02:39:55] strobegen вышел(а) из комнаты
[02:42:50] Zbroyar вошёл(а) в комнату
[02:42:55] Zbroyar вышел(а) из комнаты
[03:15:08] akovbovich вышел(а) из комнаты
[04:10:16] komar вошёл(а) в комнату
[04:10:23] gds вошёл(а) в комнату
[04:21:17] tilarids вошёл(а) в комнату
[04:38:18] tilarids вышел(а) из комнаты
[04:39:39] tilarids вошёл(а) в комнату
[04:47:24] tilarids вышел(а) из комнаты
[04:53:00] tilarids вошёл(а) в комнату
[05:14:43] Zbroyar вошёл(а) в комнату
[06:39:00] strobegen вошёл(а) в комнату
[06:39:54] tilarids вышел(а) из комнаты
[06:40:10] tilarids вошёл(а) в комнату
[09:05:50] tilarids вышел(а) из комнаты: Machine going to sleep
[09:47:41] komar вышел(а) из комнаты: Replaced by new connection
[09:47:41] komar вошёл(а) в комнату
[10:58:58] komar вышел(а) из комнаты: Logged out
[11:15:38] ermine вошёл(а) в комнату
[11:46:12] <ermine> кого нет?
[11:48:43] Kakadu вошёл(а) в комнату
[12:02:26] Typhon вошёл(а) в комнату
[12:11:58] <Kakadu> ermine: null pointer exception
[12:15:44] f[x] вошёл(а) в комнату
[12:16:14] <ermine> Kakadu: а он нужен?
[12:17:08] ermine торжественно проделала два упражнения для coq, чуть не вспотела, пока не догадалась, что ошибка из-за того, что пишешь = вместо := в определениях
[12:19:14] <Kakadu> тут везде сарказм
[12:22:53] <ermine> null нужен только в reference types, а такие есть в камле?
[12:24:47] <Kakadu> строки?
[12:25:19] <Kakadu> и вообще твое утверждение неверно
[12:33:59] akovbovich вошёл(а) в комнату
[13:06:23] komar вошёл(а) в комнату
[13:54:48] Zbroyar вышел(а) из комнаты
[14:02:19] Typhon вышел(а) из комнаты
[15:24:26] Typhon вошёл(а) в комнату
[15:24:40] komar вышел(а) из комнаты
[15:24:42] komar вошёл(а) в комнату
[15:34:06] f[x] вышел(а) из комнаты
[15:38:23] komar вышел(а) из комнаты
[15:40:05] Typhon вышел(а) из комнаты
[15:51:33] <gds> в caml-list говорят, что слово "slave" использовать неполиткошерно.  Если кто хочет приколоться -- отпишите что-то типа "Я -- потомственный дворянин, и до сих пор держу в своём замке рабов, поэтому можно я всё-таки буду использовать слово slave?".
[15:52:49] <Kakadu> А на современных винчах ещё джамперы стоят на переключение режимов master|slave?
[15:54:29] <gds> современные -- sata, там такого нет.
[15:55:37] komar вошёл(а) в комнату
[15:58:41] <ermine> ух, задание - написать факториал на коке, ща подумаем...
[16:01:02] <gds> ermine: чо тут думать -- писать надо.
[16:01:39] <ermine> gds: уже, щас потестируем
[16:02:11] <gds> ermine: заодно посмотри, на случай, если надо будет отладить факториал, в https://bitbucket.org/gds/coq-breakpoints/src/tip/Bp_examples.v , в первый пример.
[16:03:02] <gds> для отладки сложной логики таки удобно уметь останавливать редукцию определённых выражений.
[16:10:39] <ermine> gds: а что такое команда Proof?
[16:11:04] <gds> ermine: это для эстонцев, не обращай внимания.
[16:11:16] <aleksey> шогп песать Proof with
[16:11:18] <gds> команда говорит, что начинается доказательство.
[16:12:14] <gds> а, ну да, Proof with тоже можно.  Только почему-то редко когда мне было нужно.
[16:14:23] <aleksey> gds: а ты с ходу не помнишь, можно в Ltac сравнивать лексикографически выражения, чтоб например везде x=y не трогать, а y=x поменять на x=y?
[16:15:05] <gds> aleksey: точно нельзя.  Но есть обход этого дела, интересно?
[16:15:40] <aleksey> ага
[16:16:16] <aleksey> а пчу не сделали интересно, нормализовывалось бы всё легче
[16:19:24] <gds> aleksey: Definition marked {A} (a : A) := a.  Далее через match goal with |- appcontext [ ?x = ?y ] => обрабатываем x отдельным Ltac'ом: change (x) with (marked x), затем переворачиваем всё найденное по appcontext [ ?y = marked ?x ].  Затем берём следующий x.  Но надо учесть, что уже помеченные не брать -- в первом матче поставить сначала ветку appcontext [ marked _ = _ ] => idtac.
[16:20:00] <gds> почему не сделали -- влом, наверное.  А про нормализацию -- да, ты прав.
[16:21:21] <aleksey> а оно не будет на каждом вызове всё переворачивать?
[16:22:13] <gds> кстати, недавно почитал просветляющее про canonical structures, http://software.imdea.org/~aleks/papers/lessadhoc/paper.pdf , вот думаю как-то попробовать это дело для нормализации.
[16:23:19] <gds> aleksey: ну, надо поставить кое-где условия типа "помеченное -- не трогаем", в виде кейсов перед переворачивающим, типа [ marked _ = marked _ ] => idtac
[16:23:39] <gds> ну и другие случаи рассмотреть, типа [ _ = marked _ ], [ marked _ = _ ], при необходимости.
[16:23:58] <aleksey> т.е. marked после этого не стирать?
[16:24:16] f[x] вошёл(а) в комнату
[16:24:39] <aleksey> а, глню
[16:24:41] <aleksey> гоню
[16:24:53] <aleksey> я неправильно прочитал :)
[16:27:34] <gds> не стирать, а потом, как добегаешься до полного удовлетворения, стереть этот marked.  Но тут проблемка есть: если будешь стирать через appcontext опять же, то под фикспоинтами оно не заматчит.  Почему -- хз, бага видимо.  В этом случае, если у тебя нет никаких предубеждений против того, что unfold делает не только unfold, можешь сделать unfold marked in *.
[16:28:48] <f[x]> самое страшное в этом всём то, что они друг друга судя по всему понимают
[16:29:23] <gds> aleksey: кстати, если напишешь это дело -- опубликуй, мне тоже такое хочется.  И думаю обобщить это на другие виды отношений.  То ли явно передавать relation_type := eq в качестве аргумента для appcontext [ relation_type ?x ?y ], то ли тайпклассы.
[16:29:39] <gds> f[x]: жжош!
[16:31:12] <aleksey> а отношения могут быть и не бинарными, например равенство отрезков AB=CD можно так в трёх местах нормализовывать
[16:31:45] <gds> а ты с сетоидами и их применениями не разбирался?  Может они помогли бы.
[16:31:51] <aleksey> не-а
[16:34:56] <gds> кстати, подход с marked был бы чертовски полезен для нормализации всякой арифметики типа a+b+c+d = b+d+a+c: пометили, довели до (marked a) + b + c + d = (marked a) + b + d + c, и так далее.
[16:35:36] <gds> чую, тут где-то гораздо более общее решение есть.  Сходить в #coq штоле с этими идеями?..
[16:36:11] <gds> или не "общее решение", а "общая техника" для равенства, сложения и прочего.
[16:36:52] <aleksey> угу
[16:40:29] Typhon вошёл(а) в комнату
[16:41:22] <gds> aleksey: в общем, сейчас мой секс с coq чуть вдали от доказательств, скорее просто "ML + хорошие типы", а потом, если не будет влом, таки поверчу эти идейки, известно на чём.  Но если решишь сделать фокус с marked на равенствах -- опубликуй где-нибудь код.
А то среди погромистов на coq и на окамле есть одно слишком большое сходство (и даже скотство) -- у всех есть какие-то полезные велосипеды, но никто не публикует их.  В результате каждый вынужден эти велосипеды переизобретать по нужде.
[16:44:18] <gds> ermine: когда будешь решать упражнения, делай периодически "Extraction имяфункции.", чтобы понимать, что во что экстрактится.  Полезное дело.  (ровно так же, как я при изучении окамла частенько смотрел осемблир -- сразу становятся понятны кишки.)
[16:46:48] <aleksey> это да, велосипеды на камле у мну здоровые :)
[16:51:14] <f[x]> а я вам расскажу почему
[16:51:17] <f[x]> потому что неймспейсов нету
[16:51:38] <ADEpt> :D
[16:52:02] <ADEpt> "когда я слышу слово namespace-ы, я хватаюсь за пистолет"
[16:52:33] <ADEpt> f[x]: что-то эпические треды в ocaml-platform по этому поводу увяли
[16:52:40] <f[x]> та ото :(
[16:53:12] <ADEpt> f[x]: я боюсь, что Alain всех задолбает, у будут namespace-ы в виде 100500 ужасных файликов с метаданными
[16:53:26] <f[x]> комитет как он есть
[16:54:03] <f[x]> запилят решение которое покроет все-все юзкесы и ни один удобным образом
[16:54:59] <aleksey> alain это который борется с camlp4?
[16:57:34] <ADEpt> aleksey: по-моему да
[16:57:41] <ADEpt> Firsch или как-то так
[17:03:02] <ermine> фриш описывал как надо писать вместо camlp4 макросы типа @aa@
[17:03:12] <ermine> тот же ужос
[17:04:30] <ermine> aleksey: а что ты делаешь в coq? чо доказываешь?
[17:06:29] <aleksey> ermine: я там иногда задачи с олимпиад решаю
[17:07:10] <aleksey> доказательства нечитабельные выходят, вот думаю как их улучшить
[17:07:49] <ermine> aleksey: неужели нет ничего более полезного чем задачи детских олимпиад?
[17:08:31] <aleksey> это развлекуха
[17:09:03] <aleksey> из полезного я только преобразования для гугловолны там делал
[17:15:42] ftrvxmtrx вошёл(а) в комнату
[17:16:07] ftrvxmtrx вышел(а) из комнаты
[17:25:38] ftrvxmtrx вошёл(а) в комнату
[17:39:25] Zbroyar вошёл(а) в комнату
[17:44:38] <ermine> gds: а чем Example отличается от Lemma?
[17:48:33] Zbroyar вышел(а) из комнаты
[17:49:26] Zbroyar вошёл(а) в комнату
[18:10:18] Zbroyar вышел(а) из комнаты
[18:11:21] <gds> ermine: Example = Definition.  Lemma = Theorem.  Всякие более извращённые ключевые слова не очень нужны мне, но смотри сама.  Но чем Example хорош -- можно потом нагрепать и прибить примеры, когда они не нужны.  А ещё хорош Goal для "неименованных Lemma/Theorem".
[18:11:49] <gds> а хотя вот я не помню, может все 4 из первых перечисленных эквивалентны.
[18:35:33] tilarids вошёл(а) в комнату
[19:06:01] ftrvxmtrx вышел(а) из комнаты
[19:19:19] UncleVasya вошёл(а) в комнату
[19:23:10] tilarids вышел(а) из комнаты: Machine going to sleep
[19:46:18] tilarids вошёл(а) в комнату
[19:55:28] komar вышел(а) из комнаты: Logged out
[20:06:51] Kakadu вышел(а) из комнаты
[20:20:02] tilarids вышел(а) из комнаты: Machine going to sleep
[20:21:53] f[x] вышел(а) из комнаты
[20:32:19] tilarids вошёл(а) в комнату
[20:49:38] Typhon вышел(а) из комнаты
[20:53:57] tilarids вышел(а) из комнаты: Machine going to sleep
[20:54:33] <ermine> gds: пока разницу не улавливаю поскольку example и все остальное так же доказываются и финишируются командой Qed
[20:59:08] <ermine> gds: вот кстати разницы между Variable и Hypotesis кажись нет, есть только художественное соглашение по их применению
[21:22:12] <gds> ermine: не знаю, может разница будет в случаях, когда Variable внутри Section.  В этом случае оно генерализуется при закрытии секции, а про Hypothesis не знаю.
[22:08:12] Kakadu вошёл(а) в комнату
[22:16:01] f[x] вошёл(а) в комнату
[22:32:31] f[x] вышел(а) из комнаты
[22:41:53] Typhon вошёл(а) в комнату
[22:48:28] ftrvxmtrx вышел(а) из комнаты
[23:14:23] Zbroyar вошёл(а) в комнату
[23:19:35] komar вошёл(а) в комнату
[23:20:31] <Kakadu> Какой прикольный баг, улыбнитесь! http://wstaw.org/m/2013/03/28/plasma-desktopmu4913.png
[23:28:50] ermine вышел(а) из комнаты
[23:35:50] Zbroyar вышел(а) из комнаты
[23:52:11] komar вышел(а) из комнаты: Logged out