Objective Caml - Четверг, 7 октября 2010

Objective Caml

ocaml@conference.jabber.ru

Четверг, 7 октября 2010< ^ >

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

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

GMT+4
[00:14:56] ermine вышел(а) из комнаты
[00:33:40] serp256 вышел(а) из комнаты
[00:40:49] ygrek вышел(а) из комнаты
[00:41:17] ygrek вошёл(а) в комнату
[01:02:50] arhibot вышел(а) из комнаты
[01:17:17] ygrek вышел(а) из комнаты
[03:37:58] Typhon вышел(а) из комнаты
[03:41:58] zert вышел(а) из комнаты
[07:17:20] iNode вышел(а) из комнаты
[07:24:18] serp256 вошёл(а) в комнату
[08:55:51] iNode вошёл(а) в комнату
[09:02:41] gds вошёл(а) в комнату
[09:06:40] serp256 вышел(а) из комнаты
[09:58:20] serp256 вошёл(а) в комнату
[10:54:03] ygrek вошёл(а) в комнату
[10:57:03] ermine вошёл(а) в комнату
[11:04:20] ygrek вышел(а) из комнаты
[11:12:58] ygrek вошёл(а) в комнату
[11:27:44] komar вошёл(а) в комнату
[11:46:36] komar вышел(а) из комнаты
[11:58:57] ygrek вышел(а) из комнаты
[12:11:57] Kakadu вошёл(а) в комнату
[12:17:04] Typhon вошёл(а) в комнату
[12:49:45] Mon вышел(а) из комнаты
[13:25:02] komar вошёл(а) в комнату
[15:23:08] komar вышел(а) из комнаты: Replaced by new connection
[15:23:09] komar вошёл(а) в комнату
[16:20:21] zert вошёл(а) в комнату
[17:23:09] <gds> околокамловое: http://gds.livejournal.com/54391.html
[17:28:10] <komar> Э, а причем тут статическая типизация?
[17:28:32] <komar> Я такое и на питоне нахреначить могу.
[17:30:24] <gds> статическая типизация при том, что значение с типом tsl гарантированно является сортированным списком.  (т.е. тип накладывает ограничения на значение.)
Или я не понял вопроса.
[17:32:14] gds away, почитаю-отвечу попозже
[17:32:19] gds вышел(а) из комнаты
[17:33:55] <komar> Или тут есть что-то еще, кроме того, что намутили функций для работы с абстрактным типом, используя которые всегда получаешь сортированный список?
[17:52:10] <olegfink> komar: ну, идея в том, что тебе системой типов отрубили возможность сделать с этим списком что-либо, не описанное в Core
[17:52:41] <olegfink> а про то, что описано внутри, мы утверждаем, что оно сохраняет некий инвариант (здесь -- отсоритированность)
[17:52:51] <olegfink> *отсортированность
[17:53:01] <olegfink> трудно после сытного обеда писать такие длинные слова
[17:54:51] <komar> А причем здесь система типов? Только при том, что не даёт руками поковырять реализацию tsl?
[17:55:21] <olegfink> вообще, статическая типизация здесь -- не цель, а средство, в ООП есть другая инкапсуляция, но для этого применения она ничем не хуже той, что предоставляет камловая система типов
[17:56:03] <komar> Ну дык ото ж.
[17:57:44] <komar> Напоминает мне о том, как я установил SLAX на унитаз.
[17:59:24] <komar> http://dump.bitcheese.net/images/irucyxo/imga1808.jpeg/preview
[17:59:35] <komar> Вроде бы и сделал, но как-то это не совсем достижение.
[18:02:35] <olegfink> не вижу аналогии.
[18:02:54] <olegfink> gds продемонстрировал pure-fp технику, решающую классическую ооп-задачу
[18:03:12] iNode вышел(а) из комнаты: Replaced by new connection
[18:03:13] iNode вошёл(а) в комнату
[18:05:31] <komar> Это классическая задача с абстрактными типами.
[18:12:10] <f[x]> кстати тип не абстрактный - мелочь но приятно
[18:20:11] ʇsʎɯ вышел(а) из комнаты
[18:28:32] gds вошёл(а) в комнату
[18:38:23] <gds> да, сейчас я тоже вижу, что нифига не достижение :)  Но ничего страшного.  Разве что отредактирую в посте, укажу, что это тупак.
[18:41:23] <komar> gds: ну ты если чего, пиши ещё, у тебя местами очень интересно получается.
[18:42:41] <gds> komar: небось, читал срач в жыжыцэ забиватора, где я включил vsl-mode?  так это в разовых количествах только получается...
[18:43:21] <komar> Гм, срачи Зефиров-Забиватор читал с удовольствием, но тебя там не помню.
[18:43:30] <komar> Хотя я не всё читал, там целая гора говна.
[18:44:52] <Typhon> http://www.google.com/search?q=zabivator+gds+vsl
[18:45:14] <komar> Эх, жалко, что с мобилы дерева нифига не видно.
[18:48:26] <olegfink> http://ideone.com/Fcvj8 -- вот, таки вспомнил c++
[18:50:21] <olegfink> правда, я через все это не протаскиваю функцию сравнения
[18:50:45] <olegfink> но думаю, благосклонный читатель мне это простит, так как суть от этого не меняется абсолютно
[18:50:46] <gds> olegfink: да, в целом так и получается, механизм тот же самый.
[18:53:20] Kakadu вышел(а) из комнаты
[18:53:42] <olegfink> непонятно, почему твой пост не достижение -- хорошо иллюстрирует, как вот это делать с истинноверной инкапсуляцией
[18:54:37] <olegfink> а вообще, никакой истинноверности нет, совершенно одно и то же и там, и здесб
[18:54:40] <olegfink> *здесь
[18:55:32] <komar> olegfink: эти достижения в developing applications with objective caml описаны.
[18:56:21] <olegfink> gds: мне вот больше интересно, что можно понавесить на функцию типа List.reverse, чтобы посчиталось, что reverse.reverse == id :-)
[18:57:14] <olegfink> komar: ну зачем читать книги, когда есть жж?
[18:58:40] <komar> Я по ней окамл учил.
[18:58:56] <komar> Так-то я за всю жизнь ни одного абстрактного типа не написал, но помню, как их делать.
[19:01:48] <gds> komar: ни одного абстрактного?  Ну ты конкретный пацан!
[19:02:08] <komar> Ну дык, простота рулит, брат.
[19:02:45] <komar> Даже если она и выводит в repl 200 строк алгебраического типа.
[19:05:16] f[x] книжку не читал, а абстрактные типы юзает :)
[19:05:41] <gds> тут риск не в простоте, а в том, что значения данного типа могут меняться где-либо неконтролируемым образом.  Да и завязка на известную структуру не всегда хорошо, если есть хоть какая-нибудь вероятность, что структура поменяется (а операции останутся те же).
[19:05:50] <gds> тьфуты
[19:06:06] <gds> * тут смысл не в простоте, а в том, что есть риск, что ..
[19:07:07] <komar> Ну, мои задачи обходились теми гарантиями, что даёт статическая типизация.
[19:09:22] <gds> в последнее время я смотрю так: если значения используются очень много где и структура с хоть какой-нибудь вероятностью поменяется -- абстрактный тип.  Если структура вероятно поменяется -- абстрактный тип.  Если пользователю запрещено знать структуру (потому что это плохо из каких-либо соображений), или если это представляет собой уровень абстракции -- абстрактный тип.  Иначе -- до первой ошибки, где будет решено: типизация или coding guide.
[19:14:52] <komar> Пишем обычный тип, если понадобиться — делаем необыч^Wабстрактным и не делаем мозги.
[19:14:53] <gds> olegfink: в простых случаях можно заменить тип списка на my_list 'a = ([Normal|Reversed] * list 'a), и там смотреть по первому компоненту.  В почти всех функциях делать нормализацию при необходимости.  Собственно, суть ml: выражения запихиваем в мета-штуки, которые вычисляем-преобразуем так, как нам надо.
Но это неспортивно, рантайм и всё такое, в общем, тупка.
[19:15:08] <komar> Вторая стадия еще у меня никогда не наступала.
[19:16:14] <olegfink> gds: ну это для совсем простого случая
[19:16:48] <olegfink> а я хочу что-нибудь понавороченней, чтоб с произвольными линейными преобразованиями. только не знаю, как
[19:17:58] <gds> говорят, это агда умеет.
[19:19:24] <olegfink> мне почему-то кажется, что это сильно тупее dependent types
[19:21:11] <gds> там не только они, там rewriting есть, по указанным законам.  это если правильно помню.
[19:22:35] <gds> я вот раз в месяц стабильно думаю про то, как в окамловской системе типов закодировать сложение натуральных чисел, и постоянно фейл.  То есть, что-то сложное на типах тут не посчитать.
С другой стороны, это не очень-то и нужно.
[19:23:43] <komar> gds: а с этого момента поподробнее. Ты что реализовать хочешь?
[19:24:21] <f[x]> все любители считать факториал в compile-time отправляются учить camlp4 и не заниматься фигнёй в базовом языке
[19:24:48] <komar> Сделай type int = One of int | Zero и переводи 3 в One (One (One Zero)))
[19:25:30] <komar> Или вы хотите делать проверки возможных значений в compile-time? По этому поводу у меня мысли кое-какие есть.
[19:25:39] <gds> f[x]: я понял, но неспортивно :)
[19:26:06] <olegfink> нет, это считать факториал системой типов неспортивно.
[19:26:14] <gds> фибоначи можно?
[19:26:34] <olegfink> только аналитической формулой.
[19:26:41] <olegfink> с arbitrary-precision fp.
[19:26:58] <gds> FFUUUUUUUUU
[19:27:19] <f[x]> всё правильно, считать факториал это очень спортивно, обязательная дисциплина для спецолимипиады
[19:28:39] <olegfink> как-то сразу представилась публика в инвалидных колясках, считающая факториал
[19:29:41] <gds> komar: хочу реализовать какие-то типы, которыми закодировать натуральные значения, и так, чтобы было какое-либо преобразование типов, "складывающее" закодированные значения. (унификация наподобие олеговского gadt.ml, либо согласен даже на просто функцию с типом n -> m -> n+m).  Цель -- например, умножение чисел с единицами измерения.
[19:31:30] <komar> А, это.
[19:33:00] Kakadu вошёл(а) в комнату
[19:33:06] Kakadu вышел(а) из комнаты
[19:41:20] <gds> f[x]: кстати, а как реализовать сложение в compile time, да так, чтобы типизация проверялась?  например, чтобы проверялись типы в коде вида:
let height = meters 2 and base = square_meters 12 in eq (mul height base) (cubic_meters 24)
[19:44:30] <f[x]> /me?
[19:44:41] <f[x]> не знаю
[19:44:55] <f[x]> наверное делается, сейчас мозг не работает
[19:47:32] <gds> понял.  сам тоже туплю аццки.
[20:00:43] Kakadu вошёл(а) в комнату
[20:01:20] Kakadu вышел(а) из комнаты
[20:28:43] serp256 вышел(а) из комнаты
[20:54:21] komar вышел(а) из комнаты
[20:58:48] Typhon вышел(а) из комнаты: Replaced by new connection
[20:58:53] Typhon вошёл(а) в комнату
[21:02:41] <olegfink> gds: по моим представлениям, camlp4 ничего про типизацию не знает
[21:03:23] <olegfink> то есть 1) тебе все равно придется протаскивать тип через нормальную типосистему -- минорная трабла 2) ошибки типов будут отлавливаться компилятором уже после препроцессинга -- мажорная трабла
[21:03:43] <gds> это приемлемо, главное что не в рантайме.
[21:04:14] <gds> но, желательно, инфу об ед.изм. не вносить в рантайм, ибо, в идеале, это штука на уровне типов.
[21:06:02] <olegfink> я не понимаю не то что как на окамле, а вообще как это сделать
[21:06:43] <olegfink> let a = input_inches ();; let b = input_cm ();; output_square_parrots (a*b) ;;
[21:06:58] <olegfink> в твоей системе совершенно легальная штука
[21:07:09] <olegfink> а где, если не в рантайме, совершать конверсию?
[21:07:46] <olegfink> в приципе, можно хранить в некой универсальной "валюте", а соответствующие input_* будут сразу конвертировать в нее
[21:07:56] <olegfink> тогда да, видимо, можно в рантайме не хранить
[21:10:48] <gds> если брать некоторые базовые единицы измерения, и рассматривать произведения их степеней (кг^1 * м^{-2}), то всё сводится к сложению степеней.  Более хитрые вещи, типа сантиметров и дюймов, таки в рантайме придётся.  Но важно, чтобы хотя бы по размерности сошлось.
[21:14:12] <olegfink> размерности, кажется, сделать проще, да
[21:15:05] <olegfink> кстати, я тут поел булочку, и осенило меня, что на c++ я выше по логу написал полную фигню: operator list<T>& нельзя делать, так как оно возвращает ссылку на нас без медного тазика, и все ломает
[21:15:33] <olegfink> надо то ли дописать куда-нибудь пару раз слово const, то ли копию возвращать
[21:18:19] <gds> ну, плюсовый код -- ровно такая же демонстрация идеи, как и моя сортировка.  Главное, что в теории допиливается.
[21:36:14] <olegfink> попробовал еще попридумывать про reverse -- нифига не придумал
[21:36:35] <olegfink> я могу это сделать, если мне известна длина списка, тогда все просто:
[21:36:43] <olegfink> reverse(i) = n - i
[21:36:50] <olegfink> в смысле индексов
[21:37:00] <olegfink> тогда reverse(reverse(i)) = n - (n - i) = i
[21:37:02] <olegfink> и все дела
[21:37:27] <olegfink> а как написать квантор по длине, я как-то плохо представляю
[21:49:52] komar вошёл(а) в комнату
[21:50:51] ygrek вошёл(а) в комнату
[22:19:54] ygrek вышел(а) из комнаты
[22:19:56] ygrek вошёл(а) в комнату
[22:33:39] serp256 вошёл(а) в комнату
[22:37:51] komar вышел(а) из комнаты
[22:41:13] gds вышел(а) из комнаты
[22:50:51] ygrek вышел(а) из комнаты
[22:50:54] ygrek вошёл(а) в комнату
[22:56:55] ygrek вышел(а) из комнаты
[22:56:57] ygrek вошёл(а) в комнату
[23:12:26] ygrek вышел(а) из комнаты
[23:13:09] ygrek вошёл(а) в комнату
[23:25:37] serp256 вышел(а) из комнаты
[23:28:51] serp256 вошёл(а) в комнату