Objective Caml - Понедельник, 14 января 2013

Objective Caml

ocaml@conference.jabber.ru

Понедельник, 14 января 2013< ^ >

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

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

GMT+4
[00:09:30] ygrek вышел(а) из комнаты
[00:09:35] ygrek вошёл(а) в комнату
[00:45:50] evilbloodydemon вышел(а) из комнаты
[03:11:57] Andrey Popp вышел(а) из комнаты
[03:26:43] ygrek вышел(а) из комнаты
[04:40:29] komar вышел(а) из комнаты: Logged out
[06:50:59] ermine вошёл(а) в комнату
[07:43:01] evilbloodydemon вошёл(а) в комнату
[08:32:30] dzhon вошёл(а) в комнату
[09:02:53] Andrey Popp вошёл(а) в комнату
[10:47:21] Sun][ вошёл(а) в комнату
[10:49:07] Sun][ вышел(а) из комнаты
[10:56:39] dzhon вышел(а) из комнаты
[11:06:42] dzhon вошёл(а) в комнату
[11:14:36] Sun][ вошёл(а) в комнату
[11:21:24] ftrvxmtrx вошёл(а) в комнату
[11:28:31] Andrey Popp вышел(а) из комнаты
[11:53:34] Kakadu вошёл(а) в комнату
[11:54:58] Kakadu вошёл(а) в комнату
[12:33:15] Zbroyar вошёл(а) в комнату
[12:33:29] Andrey Popp вошёл(а) в комнату
[12:33:29] Typhon вошёл(а) в комнату
[12:37:47] komar вошёл(а) в комнату
[12:49:50] Andrey Popp вышел(а) из комнаты
[13:06:32] Typhon вышел(а) из комнаты
[13:20:20] Typhon вошёл(а) в комнату
[13:28:06] Zbroyar вышел(а) из комнаты
[13:29:24] Andrey Popp вошёл(а) в комнату
[13:36:45] evilbloodydemon вышел(а) из комнаты
[13:37:56] evilbloodydemon вошёл(а) в комнату
[13:43:59] evilbloodydemon вышел(а) из комнаты
[13:45:08] Andrey Popp вышел(а) из комнаты
[13:46:54] Zbroyar вошёл(а) в комнату
[13:56:58] evilbloodydemon вошёл(а) в комнату
[14:03:57] Andrey Popp вошёл(а) в комнату
[14:09:46] Andrey Popp вышел(а) из комнаты
[14:50:28] <gds> есть у меня ast кучи функций, где типов почти нигде нет, но они выводятся из внешнего окружения.  (то, что типов нет, это нормально, по-другому не могу в этой задаче.)
и вот, по условию задачи, считаем, что всё в конце концов протипизировать таки можно, но далеко не за один проход.
как бы я поступил в простом-тупом случае: взял бы ref (option type) и заполнял бы типы по мере возможности.  Но из-за некоторых обстоятельств я не могу использовать ни изменяемые типы, ни даже lazy.  только чистая функциональщина.
как бы вы в этом случае выкрутились?
[14:56:05] Typhon вышел(а) из комнаты
[15:19:37] klapaucius вошёл(а) в комнату
[15:20:37] Typhon вошёл(а) в комнату
[15:25:48] <Kakadu> gds: А структуру типа ast ты варьировать можешь или прибита гвоздями?
[15:30:23] Typhon вышел(а) из комнаты
[15:30:54] Typhon вошёл(а) в комнату
[15:43:33] Andrey Popp вошёл(а) в комнату
[16:07:06] <gds> Kakadu: варьировать приходится.  Более того, как минимум две их будет: нетипизированная и типизированная.  И, думаю, что-то промежуточное будет.  Но какое и как -- не представляю.
[16:09:50] <Kakadu> gds: Может иногда выполнять ast_items |> List.map partially_infer_types?
[16:10:11] <Kakadu> Будет по чуть-чуть выводить
[16:10:18] <Kakadu> и без мутабельности
[16:10:21] <Kakadu> костыльно правда
[16:11:41] <gds> ок, но проблемой является ещё и partially_infer_types, которая должна как-то хранить и выведенные, и ещё не выведенные типы.
(более того, но это за рамками моего вопроса, нужно обеспечить доказанную завершимость этой процедуры, кроме случаев, когда типы вывести нельзя.  нувыпонели, на чём я пишу.)
[16:12:43] <gds> то есть, надо будет "расщеплять" каждый узел аст так, чтобы там было либо выведенное, либо ещё не выведенное.  Или ещё какую-нибудь срань исполнять.
[16:13:30] <Kakadu> None --- невыведеннное, Some _ -> выведенное
[16:14:20] <Kakadu> partially_infer_types будет выплёвывать деревяшку где некотороые None превратились в Some
[16:15:52] <Kakadu> А насчет доказуемости, что-то было у пирса, типа если у нас типизированное ляюмбда исчисление с fix-point комбинатором но _без_ общей рекурсии, то типы выводимы
[16:16:00] <Kakadu> Я не помню уже точно.
[16:16:09] <Kakadu> Но тут возникает вопрос, что у тебя за ast?
[16:16:54] <Kakadu> Я так понимаю петушок не любит мутабельности, потому что в этом случае вообще сложно что-то доказать?
[16:24:40] <gds> Kakadu: а вроде логично -- к каждому узлу присобачить option type.
про пирса -- да, чото есть.  но я могу себе позволить сказать "не выводится никак, расставляй типы".  Потому что в "здоровых" случаях выводиться таки будет.  А завершимость -- например, подсчётом количества None/Some.  Если количество не изменилось -- выходим с тем, что есть.
кококо вообще не умеет мутабельность, а тащить манатки неохота.  но мне корректность инферринга доказывать не нужно, поэтому мутабельность -- всего лишь вопрос удобства при написании кода.
[16:27:17] <gds> (как хорошо, что у меня вопрос про чистый окамл без ленивых значений, а не про coq, иначе оффтопик был бы!)
[16:44:03] <Kakadu> Ну и хорошо)
[16:46:55] Andrey Popp вышел(а) из комнаты
[16:54:58] Typhon вышел(а) из комнаты
[16:57:56] Zbroyar вышел(а) из комнаты: Replaced by new connection
[16:57:57] Zbroyar вошёл(а) в комнату
[16:58:36] Sun][ вышел(а) из комнаты
[17:10:46] Typhon вошёл(а) в комнату
[17:11:03] Zbroyar вышел(а) из комнаты: Replaced by new connection
[17:11:04] Zbroyar вошёл(а) в комнату
[17:29:46] Andrey Popp вошёл(а) в комнату
[17:30:14] Andrey Popp вошёл(а) в комнату
[17:30:19] Andrey Popp вышел(а) из комнаты
[18:29:20] dzhon вышел(а) из комнаты
[18:38:43] Andrey Popp вышел(а) из комнаты
[18:41:23] Andrey Popp вошёл(а) в комнату
[18:52:26] Andrey Popp вышел(а) из комнаты
[18:58:59] Andrey Popp вошёл(а) в комнату
[19:08:20] Kakadu вышел(а) из комнаты
[19:11:28] Kakadu вышел(а) из комнаты
[19:27:33] ftrvxmtrx вышел(а) из комнаты
[20:04:39] Typhon вышел(а) из комнаты
[20:08:59] Typhon вошёл(а) в комнату
[20:14:43] Typhon вышел(а) из комнаты
[20:22:08] komar вышел(а) из комнаты: Logged out
[20:32:11] f[x] вошёл(а) в комнату
[21:29:07] Andrey Popp вышел(а) из комнаты
[21:58:06] Zbroyar вышел(а) из комнаты: Replaced by new connection
[21:58:07] Zbroyar вошёл(а) в комнату
[22:00:43] ludovik вошёл(а) в комнату
[22:41:02] Andrey Popp вошёл(а) в комнату
[22:53:17] evilbloodydemon вышел(а) из комнаты
[22:53:29] evilbloodydemon вошёл(а) в комнату
[23:51:02] Andrey Popp вышел(а) из комнаты