Objective Caml - Воскресенье, 4 ноября 2012

Objective Caml

ocaml@conference.jabber.ru

Воскресенье, 4 ноября 2012< ^ >

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

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

GMT+4
[01:40:28] Kakadu вышел(а) из комнаты
[01:46:21] tilarids вошёл(а) в комнату
[03:24:54] Andrey Popp вышел(а) из комнаты
[03:31:25] tilarids вышел(а) из комнаты
[03:31:35] tilarids вошёл(а) в комнату
[05:16:16] akovbovich вошёл(а) в комнату
[06:49:47] letrec вошёл(а) в комнату
[10:37:09] Andrey Popp вошёл(а) в комнату
[10:38:58] Kakadu вошёл(а) в комнату
[10:49:15] UncleVasya вошёл(а) в комнату
[11:41:41] letrec вышел(а) из комнаты
[12:13:28] ermine вошёл(а) в комнату
[12:53:23] komar вошёл(а) в комнату
[13:51:21] letrec вошёл(а) в комнату
[13:51:31] letrec вышел(а) из комнаты
[13:51:46] letrec вошёл(а) в комнату
[14:08:08] f[x] вошёл(а) в комнату
[14:39:41] tilarids вышел(а) из комнаты: Machine going to sleep
[14:42:33] UncleVasya вышел(а) из комнаты
[16:29:16] Andrey Popp вышел(а) из комнаты
[16:37:56] Andrey Popp вошёл(а) в комнату
[17:08:08] Andrey Popp вышел(а) из комнаты
[17:10:05] Typhon вошёл(а) в комнату
[17:23:10] Andrey Popp вошёл(а) в комнату
[17:23:22] Andrey Popp вошёл(а) в комнату
[17:23:33] Andrey Popp вышел(а) из комнаты
[17:26:34] Andrey Popp вышел(а) из комнаты
[18:16:54] tilarids вошёл(а) в комнату
[18:24:49] <tilarids> а какие есть способы профилировать память в окамле? Мне интересно, что занимает память
[18:25:41] <tilarids> точнее, у меня есть список из 75kk float*int и он занимает 5 гиг
[18:26:07] <komar> зойчем они тебе?
[18:26:38] <tilarids> komar, так, задачку решаю, решил на окамле делать
[18:26:51] <komar> Может, это, поточно да лениво?
[18:28:52] <komar> Олсо, зделой на J
[18:29:03] <komar> Или на K
[18:29:06] <komar> Тырпрайзнее.
[18:29:08] <tilarids> не, мне нужно список создать, его отсортировать, потом по нему пробежаться и найти первое вхождение, которое меня устроит
[18:29:25] <tilarids> и чтобы это шустренько было
[18:29:35] <komar> man sort
[18:29:36] <komar> man grep
[18:29:46] <komar> Не?
[18:30:13] <tilarids> я ожидал, что 75kk float*int займут один гиг памяти, а оно занимает 5 гиг. Почему - не пойму
[18:31:15] <Kakadu> тэг одного, тэг второго и тэг пары
[18:31:28] <komar> Олсо, может, сначала таки выбрать устраивающее, а потом его сортировать?
[18:32:31] <tilarids> сейчас, я вырезал кусок кода - http://codepad.org/VU4NgIMz . Кодепад его не компилит из-за comprehension, но вроде должно быть правильно
[18:33:17] <tilarids> так вот, я сортирую по угловым координатам и потом ищу подходящий, выбрать, а потом отсортировать - не выйдет
[18:34:01] <tilarids> Kakadu, а как уменьшить потребление? Плюс, что-то медленновато работает, по непонятным мне причинам
[18:34:24] <Kakadu> байткод?
[18:34:28] <tilarids> opt
[18:35:02] <tilarids> ocamlfind ocamlopt -package batteries,batteries.pa_comprehension.syntax -syntax camlp4o -linkpkg file.ml -unsafe -inline 20 -o output
[18:36:05] <Kakadu> ты что, ищешь все целые точки, которые лежат в окружности?
[18:36:25] <tilarids> Kakadu, среди них ищу, да
[18:37:54] <tilarids> чтобы получить 75кк нужно 10000, а не 100
[18:38:01] <ermine> задачка с фпрога про osm?
[18:38:19] <tilarids> ermine, задачка с ibm ponder this этого месяца :)
[18:38:41] <tilarids> сначала нужно переборное решение хоть какое-то получить, а потом искать красивое решение
[18:41:33] ermine выкинула lazy из своего кода и пытается тоже чота решить
[18:41:54] <Kakadu> tilarids: если совсем мы никак не поможем --- сходи к буржуям в ирку
[18:49:19] <tilarids> ermine, ponder this пробуешь?
[18:49:31] <tilarids> переписал быстренько на плюсах - http://codepad.org/MhrE7eaX
[18:49:56] <tilarids> 96kk элементов - 1.4 гига
[19:01:04] <tilarids> а где сидят правильные буржуи? На фриноде или еще где?
[19:01:20] <komar> Там.
[19:01:23] <komar> И еще в caml-list.
[19:01:45] <tilarids> ну, подождем тогда
[19:02:15] <tilarids> или, как вариант, не выделываться, а писать все на плюсах
[19:09:41] <ermine> на go lang
[19:09:58] <ermine> это же язык будущего!
[19:11:51] <klapaucius> Надеюсь, что это будущее никогда не станет настоящим.
[19:12:01] <tilarids> я все ищу и ищу язык будущего
[19:12:30] <tilarids> и все равно ничего лучше плюсов найти не могу, а это само по себе звучит смешно
[19:17:21] <gds> tilarids: если хочешь реально быстро -- сделай array/bigarray на каждый компонент тупла и реализуй какой-нибудь qsort поверх двух массивов.
Почему так -- 1. работа со списками -- дольше, обычно, чем с массивами.  2. если не будет в памяти тупла -- не будет тега этого тупла, нужного для мусорщика.  3. если запихать плавучку в массив, на каждое плавучее значение получишь минус один тег и минус одно значение в памяти (последнее важно для быстрой работы мусорщика в том числе).
[19:18:32] <gds> всё вот хочу запилить функцию, сортирующую 2 массива (условно, array 'a и array 'b), где сравнение имело бы тип " 'a -> 'b -> 'a -> 'b -> int ".  часто нужно.
[19:18:44] <gds> начать можно было бы с копипасты Array.sort.
[19:19:37] ermine решила погрызть книжку по coq
[19:19:58] <gds> кстати, статья про coq, в плане содержимого, вполне готова.  Но многое нужно исправить, в мелочах нужно дополнить.
[19:20:49] <ermine> большая статья?
[19:21:15] <ermine> ... которую будет нереально прочитать
[19:21:54] <gds> разумеется.  Конечно, начиная с 10го абзаца там будет полная ахинея, но, всё равно, кто ж дочитает.
[19:23:02] <ermine> gds: кстати сегодня в другом чате я спрашивала что такое reflexivity
[19:23:11] <gds> а в каком?
[19:23:24] <ermine> gds: всё же эту книжку надо начинать со чтения чего-то по матлогике
[19:23:34] <gds> не нужно.
[19:23:41] <ermine> gds: в тусовочном
[19:24:15] <ermine> чтобы понять при чем тут reflexivity, пришлось заглянуть на википедию и осилить примерно про эквивалетность
[19:25:28] <ermine> gds: еще не очень недавно я не знала, что теоремы доказываются индукцией (в математике) даже в школах, а не только в coq и как это по-школьному выглядит
[19:25:28] <gds> это тебе ещё не рассказывали про эквивалентность/конгруэнтность, рисуя стрелки в категориях.  В вики всё понятно.
[19:26:05] <ermine> gds: я о том, что тупой блондинке точно не хватит даже навыков программирования в таком крутом языке, как камло
[19:26:14] <gds> разные теоремы бывают, и в разных системах логики/типов по-разному.  Но да, если есть индуктивная структура данных, то вещи про неё, конечно, индукцией.
[19:26:33] <gds> ты ж вроде брюнеткой была.
[19:27:24] <ermine> ну какая разница
[19:27:57] <ermine> и твою статью, боюсь, осилят только те, кто недавно учился в вузах по соответствующему профилю и при этом не прогуливали лекции
[19:28:19] <gds> нет, там специфики мало будет, и будет интересненько, чисто "пенки с поверхности".
[19:28:53] <ermine> gds: чо, совсем нет слов "индукция" и "рефлексивность"?
[19:29:43] <tilarids> gds, как-то это все так неприятно, я не ожидал от окамля такого подвоха :( Более того, заюзав Array я получаю ситуацию еще похуже, хотя непонятно, как
[19:29:45] <gds> индукция -- если и есть, то только по отношению к типам данных.  рефлексивность -- это идея, надо добавить.  баззворды же!
а вообще, надо из-за того, что я там описал подход с decidable equality, но нужно описать и альтернативы.
[19:31:09] <ermine> а какую задачку в качестве примера решаешь там?
[19:31:10] <gds> tilarids: каждое значение в окамле (тупл тоже) имеет какой-то тег.  Что ж тут неожиданного.
Про array -- там могут быть моменты различные.  Сходу не знаю, конкретно надо смотреть.
[19:31:54] <tilarids> gds, отсюда и первая часть вопроса - есть какой-либо memory profiler? Который бы показал мне размеры выделенных объектов?
[19:33:06] <gds> ermine: я там не решаю задач, я описываю впечатления от решения одной задачи.
[19:33:29] <tilarids> вот версия с array http://codepad.org/oeHElsPM
[19:34:37] <ermine> gds: а, ну, впечатления.... надеюсь не очень грустные
[19:35:18] <gds> tilarids: можешь мой objsize взять, http://forge.ocamlcore.org/frs/download.php/442/objsize-0.16.tar.gz
[19:36:33] <ermine> gds: ты еще там монады в coq заверни!
[19:37:05] <gds> tilarids: код посмотрел.  Слишком сурово.  Нужно вполне понимать, во что оно компилируется, если хочешь производительности.  Например, те же enum'ы.  Я -- не понимаю (не работал с ними особо), поэтому посоветовать ничего не могу.
[19:37:32] <gds> ermine: впечатления -- 50/50.  Про монады тоже завернул, и про трансформеры.
[19:38:03] <ermine> gds: ждём crap release
[19:41:05] <ermine> gds: я кстати так и никак не могу научиться читать induction principle, как они выводятся по команде check
[19:41:16] <ermine> отсутствие скобок мешает
[19:42:07] <ermine> каша из фораллов и сигнатур предикатов
[19:42:39] Andrey Popp вошёл(а) в комнату
[19:43:13] <gds> ermine: а не нужно эти принципы использовать в явном виде.  Когда будет нужда (а у меня не было; разве что для интереса) -- прочитаешь.
[19:43:54] <gds> ermine: если хочешь поиграться -- возьми типы (точнее, их аналоги) -- unit, bool, option, и на их принципы посмотри.
[19:46:38] <ermine> gds: ну принцип начиная уже у unit вгоняет в тоску начиная с forall u
[19:47:40] <ermine> чо за такой любой u?
[19:56:53] <tilarids> gds, exactly! Я не понимаю, во что оно компилируется. В плюсах/джаве/питоне - понимаю. В хаскеле/окамле - не понимаю. Что прочитать, чтобы понять?
[19:57:08] <ermine> интересно, есть ли среди нас хоть один натуральный блондин?
[19:58:24] <Andrey Popp> tilardis, а ты на самом деле можешь понять во что C++ компилируется с -O3 и прочим? Оно же по-моему даже от версии к версии различается
[19:58:32] <ermine> tilarids: стоит написать хоть один сишный биндинг к камлу, как подобное прозрение сразу наступает
[19:59:03] <Typhon> да
[20:00:06] <tilarids> Andrey Popp, на плюсах я очень давно пишу, поэтому я с большой долей вероятности могу сказать, во что компилируется тот или иной код
[20:01:04] <tilarids> про биндинги - я на окамль смотрю исключительно ради того, чтобы заменить им сишный код. Зачем мне к сишному заменителю сишные биндинги? :)
[20:01:04] <ermine> любой язык транслируется в машкоды
[20:01:26] <ermine> видимо и код в coq тоже, что обнадеживает
[20:02:36] <ermine> а мой супруг утверждает, что вообще все языки одинаковы
[20:34:47] ludovik вошёл(а) в комнату
[20:35:58] <tilarids> кстати, попробовал на скале то же самое, 5 гигов памяти ему не хватило
[20:38:49] <ermine> я тоже так умею, у меня в тестах xml не всегда хватает машинной памяти на пережевывание двухгигабайтного файла
[20:40:00] <ermine> тоже не хватает 5 гигов на то, чтобы построить в памяти всю структуру хмля
[20:40:33] <Andrey Popp> регэкспами его
[20:41:06] <ermine> структуру построить, а не распарсить
[20:41:14] <Andrey Popp> а, ок
[20:41:31] <ermine> надо будет в следующий раз попробовать кэшировать тэги хмля
[20:41:50] <ermine> и вообще регэкспы - это и так плохая идея
[20:45:58] <tilarids> ermine, кешировать или хэшировать? Мы хэшируем, это по оценкам еще и ускоряет парсинг в 6 раз :)
[20:46:08] <komar> ПИШИТЕ НА ПИТОНЕ СРАНЫЕ НИЩЕБРОДЫ ПЛАНКА ПАМЯТИ НА 4GB 500 РУБЛЕЙ СТОИТ
[20:47:12] <komar> Не, серьезно, мне это в последнее время постоянно говорят.
[20:47:25] <komar> Я даже поверил в это чуть-чуть.
[20:53:42] letrec вышел(а) из комнаты
[20:56:42] <tilarids> на питоне: 5.6 гб, а потом его убивает oom_killer
[20:58:46] <tilarids> из мейнстримового неопробованного остался js, haskell, plain java и C#
[20:59:46] <komar> http://bitcheese.net/art_thou/images/full/sticks/ruby.png
[21:01:33] <Andrey Popp> tilardis, на Scala что использовал? Array?
[21:04:40] <ermine> надо на голанге, а не на питоне
[21:06:14] <tilarids> Andrey Popp, не, я list comprehension юзал, поэтому листы
[21:06:29] <Andrey Popp> tilardis, ну тогда чему удивляться
[21:06:49] <tilarids> вот скала меня ни капли не удивила :)
[21:07:27] <Andrey Popp> вообще непонятно зачем использовать списки чтобы числа крошить
[21:08:15] <Andrey Popp> а на python без numpy?
[21:10:05] <tilarids> конечно. Я писал на каждом языке так, как на нем обычно пишут. Без извращений. Так, я не заюзал сишный qsort в плюсовом коде, не разбивал таплы в окамле на два массива, не юзал numpy и cython. И я хочу получить нормальный результат не отказываясь от приятных плюшек языков
[21:11:38] <tilarids> так, я не знаю простого и приятного способа создания такого Array в scala без предварительного создания списка
[21:11:58] <tilarids> array comprehension в скале нет, насколько я знаю
[21:12:00] <Andrey Popp> скинь код на Scala
[21:12:30] <tilarids> http://codepad.org/Das6rGZH
[21:13:06] <tilarids> res.sorted только нужно, это я уже опосля закомментил
[21:13:45] <tilarids> скала порадовала тем, что умудрилась этот код распараллелить на все мои процы, заняв под 40 минут чистого процессорного времени прежде, чем упасть по OutOfMemory
[21:14:39] <tilarids> и питоновский код, кому интересно
[21:14:41] <tilarids> http://codepad.org/qkvR2New
[21:15:11] dzhon вошёл(а) в комнату
[21:16:44] <ludovik> так это хорошо или плохо?
[21:18:08] <tilarids> ludovik, то, что смогла - офигенно. То, что ничего при этом не сделала и упала - фиговастенько :(
[21:20:32] <Andrey Popp> tilardis, странно, этот код не должен был распараллелится, а чем память измерял?
[21:22:45] <tilarids> банально - топом
[21:22:54] <Andrey Popp> как запускал?
[21:23:13] <tilarids> JAVA_OPTS="-Xmx5g" scala Ibm
[21:26:46] <Andrey Popp> process_coord какой-то странный, зачем там flatMap? зачем case не на tuple?
[21:26:57] <gds> ermine: для любого значения с типом unit, конечно.
[21:27:16] <gds> tilarids: ну пиши проще, всяко понятнее будет, во что компилируется, и даже более оптимизируемо.
[21:27:17] <Andrey Popp> tilardis, вообщем у меня больше 2.77 ещё не поднималось, но пока считает
[21:28:07] <gds> tilarids: если хочешь окамлом заменить сишное, то учти, что не всегда тебе захочется переписывать готовые сишные либы на окамл.
[21:28:40] <gds> регекспами xml -- свежая идея!
[21:28:45] <tilarids> так а я и не собираюсь переписывать сишные либы. Сишному - сишное. Мне окамль для веба нужен
[21:28:53] <ermine> gds: вообще хвост подобных принципов не нравится, он традиционно выглядит как P a, ну зачем это?
[21:29:41] <Andrey Popp> gds, ну это больше саркастическое предложение было, но если регэксп поверх не chars, а элементов, то почему бы нет, если xsd задаёт регулярный язык, а таких много
[21:29:58] <tilarids> Andrey Popp, потому что я хочу получить список таплов, а не список списков таплов, и не список таплов таплов. Мне отсортировать потом нужно. Ну, а default case руки сами пишут
[21:30:49] <gds> ermine: затем, что "для любого утверждения P, если оно верно для каждого компонента типа, оно верно для любого значения типа".  Если a это значение, что P a означает, что свойство для него верно.
[21:40:16] <ermine> gds: принцип - это прога или рисованные типы?
[21:40:40] <gds> в каком смысле?
[21:41:20] <ermine> gds: ну вот по unit_ind не видно что будет с P tt
[21:42:33] <ermine> в начале и конце описания уже написаны типы
[21:42:45] <gds> ну, любое значение P с типом unit -> Prop можно присунуть в этот принцип индукции и, доказав, что P tt верно, получить доказательство того, что "для любого a : unit, P a верно".
[21:43:20] <ermine> в смысле forall P : unit -> Prop, ... forall u: unit, P u
[21:43:50] <gds> первое -- типа fun (P : unit -> Prop), последнее -- типа (fun (u : unit) -> P u).
[21:44:04] <gds> ну, unit -- вырожденный случай.  Погляди на другие тоже.
[21:44:30] <gds> да и вообще, оно тебе надо, досконально разбираться с этим?  Мне не надо было, да и сейчас хз зачем оно есть в голове.
[21:44:39] <ermine> ну а как в этом участвует P tt?
[21:45:47] <ermine> gds: а как можно читать рекомендованную тобой книжку, если в ней понимаешь только одно слово из сотни
[21:47:40] <gds> ну смотри.  Inductive unit := | tt : unit.  Тут, чтобы доказать утверждение про любое значение типа unit, достаточно доказать, что утверждение верно для всех веток этого типа.  Если утверждение верно в случае, когда a = tt, то для любого u : unit это утверждение тоже верно.  В данном случае слишком тривиально, бери другие случаи.  Например, bool.
И там будет принцип вида "если есть свойство P, берущее булевое значение, и если оно верно для true, и если оно верно для false, то оно верно и для любого булевого значения".
[21:48:14] <ermine> мне в тусовочном чате намекнули так, что я поняла, что читаю -> как выводилку типов, а не импликацию
[21:48:30] <ermine> всё же нужны прочные основы матлогики
[21:49:05] <ermine> так-то вот
[21:49:40] <gds> -> это в любом случае не выводилка типов, это просто тип функции.  А матлогика -- навряд ли.  Тут есть Hurry-Coward correspondence, которое утверждает, что "для любого a : t, u" -- это как бы "fun (a : t) -> (значение : u)".
[21:52:53] <ermine> gds: P u в хвосте описания unit_ind - это применение предиката или непривычное описание типа?
[21:54:54] <ermine> параметрического видимо
[21:57:31] <gds> это и описание типа, и факт того, что при применении всех аргументов к функции "принцип индукции" мы получим утверждение P u.  То есть, если P : unit -> Prop, то P u : Prop, то есть, есть какой-то тип, находящийся в Prop.  А какое именно значение данного типа получим -- не суть важно.  Важно то, что каким бы ни был P : unit -> Prop, мы получим в итоге значение, находящееся в Prop.
[22:01:35] <ermine> как всё сложно
[22:03:44] ermine за сегодня прочитала 5 страниц книжки по coq - это много или мало?
[22:23:23] ludovik вышел(а) из комнаты
[22:43:49] <gds> ermine: кстати вот, индукция по списку, если её рассмотреть в терминах значений, а не доказательств, выглядела бы так: "мы знаем, как из пустого списка получить значение типа A, и знаем, как из головы и значения типа A, полученного для хвоста списка, получить значение типа A для списка, состоящего из данной головы и данного хвоста".  Что-то напоминает?
[22:55:46] <ermine> gds: это выглядит как A -> B -> C -> D, если смотреть на кукушную картинку, где A - пустой список, B - из головы и тд, вот тут абсолютно не клеится с тем, что видишь в сигнатуре для камла, потому что уже надо читать "если A верно, то tckb B верно, то если C верно и так дальше...
[22:56:13] <ermine> ужас тихий, когда нет стереометрии в глазах
[22:56:23] <gds> параллель: "значение типа A" = "свойство P верно для списка либо его части".
[22:57:49] <ermine> пока не вижу параллели
[22:59:13] <ermine> ну хотя бы потому что хочу видеть перечисление вариантов через палочку, а не стрелочки
[23:00:00] <ermine> ну не будешь же на камле писать fun [] -> fun (x::xs) -> true
[23:07:05] ermine похоже нашла таки куда воткнуть lazy в свой xsd, чтобы не циклилось в undefined и теперь есть годный результат, ура
[23:07:31] <gds> зато буду писать
value ... (for_nil : 'r) (for_cons : 'a -> 'r -> 'a) (lst : list 'a) : 'r
[23:08:24] <komar> ermine: это.
[23:08:30] <komar> Ты в курсе, что у меня есть разбор xsd на lazy?
[23:08:42] <komar> Там, конечно, говнище такое, что мне смотреть страшно, но все же.
[23:08:49] <gds> вот, считай, 'r кое-как связано с P.  for_nil получает всю информацию о голове списка (а именно -- ничего) и возвращает значение 'r, например.
[23:09:08] <komar> Гы, кстати, я этот разбор не сам писал.
[23:09:19] <ermine> komar: он читает XMLSChema.xsd?
[23:09:30] <komar> Че-е?
[23:09:38] <komar> А.
[23:09:39] <ermine> который весь приведен в старой спеке xsd
[23:09:43] <komar> Ну да, он читает .xsd, да.
[23:09:55] <komar> http://komar.bitcheese.net/en/code/xmlfuzzer
[23:10:00] <komar> Вот это говно как работает, по-твоему?
[23:10:19] <ermine> и не сыплется на рекурсивных complextype?
[23:10:28] <komar> http://dump.bitcheese.net/images/ixojitu/snapshot10.png — оно вордовкие файлы автоматом генерит!!!!1111
[23:10:33] <komar> Слушай, не рассказывай мне тут.
[23:10:39] Typhon вышел(а) из комнаты
[23:10:58] <komar> Я дро^Wеба^Wреализовывал ooxml. Есть что-то хуже?
[23:11:05] <komar> Ах да, вспомнил, svg.
[23:11:11] <ermine> ну ты крут, в дверь с раскинутыми веером пальцами пролазишь?
[23:11:12] <komar> Там все на регэкспах.
[23:11:23] <komar> Которые мне таки влом было реализовывать.
[23:11:33] <komar> Хотя был какой-то генератор готовы, на х-ле.
[23:12:08] <komar> ermine: да я король говноедов.
[23:12:32] <komar> Но суть в том, что да, есть у меня парсер, который парсит даже ooxml. А рекурсивных типов там черти сколько.
[23:13:02] <ermine> кого генерит? png?
[23:13:20] <komar> Хто?
[23:13:41] <komar> Фазер генерит xml. Генератор тот на х-ле генерил текст из регэкспов.
[23:13:45] <komar> О чем я еще тут говорил?
[23:14:17] <ermine> а, тебе хмл генерить
[23:14:27] <komar> Да пофигу.
[23:14:34] <komar> Там парсинг xsd в отдельном модуле.
[23:15:00] <komar> Я, правда, уже под угрозой смерти не вспомню, чего там написано, но это помню точно.
[23:17:27] <ermine> ща всосаю даркс и посмотрю как ты решил ту проблему
[23:17:48] komar закрылся руками.
[23:19:38] f[x] вышел(а) из комнаты
[23:20:22] <ermine> мда, все тырят код друг у друга, кроме одного великого
[23:20:58] <ermine> я правда не пошла по этому пути
[23:21:49] <gds> это не "тырить", это code reuse.
[23:22:38] <gds> хотя, стоп.  куда я пишу.
[23:23:21] <ermine> в гугль
[23:25:40] <gds> ermine: ну, асилила про fold_right?
[23:26:55] <ermine> gds: (в замешательстве) а что было про fold_right?
[23:27:26] <gds> (2012-11-04 21:00:00) ermine: ну не будешь же на камле писать fun [] -> fun (x::xs) -> true
(2012-11-04 21:07:31) gds: зато буду писать
value ... (for_nil : 'r) (for_cons : 'a -> 'r -> 'a) (lst : list 'a) : 'r
[23:28:22] <ermine> а где тут фолд без изначального значения?
[23:28:55] <gds> в индукции база -- это как бы начальное значение.  "для пустого списка".  for_nil тут.
[23:30:44] <ermine> пожалуй, похоже
[23:31:52] <ermine> а нет, не похоже
[23:31:58] <ermine> в фолде результат 'a
[23:35:49] <komar> ermine: ой, совсем забыл.
[23:35:54] <komar> У меня там окамледусе.
[23:35:58] <komar> Не пользуйся этой херней.
[23:36:01] <komar> Не надо.
[23:36:04] <komar> Пожалуйста.
[23:36:48] <ermine> komar: да у меня всяко свои цели
[23:37:55] <gds> действительно, свёртка и индукция -- не совсем одно и то же.  но:
Check list_rect.
list_rect
     : forall (A : Type) (P : list A -> Type),
       P nil (* если получим значение "P nil", *) ->
       (forall (a : A) (l : list A), P l -> P (a :: l)) (* и если для каждого значения для хвоста, "P l", и для каждой головы "a" можно получить значение для списка из этой головы и этого хвоста, "P (a :: l)", *) ->
       forall l : list A, P l  (* то для любого списка l можем получить значение "P l" *)
если в терминах доказательств, то "значение "P x"" замени на "факт P, известный про список x".
[23:43:27] <ermine> komar: это уже стало более понятнее как читать, но всё равно не очень привычно, но стало чуток легче, спасибо
[23:53:32] ermine вышел(а) из комнаты
[23:57:43] gds вышел(а) из комнаты