Зарелизил мелкую библиотечку для отладки редукций выражений в пределах coq: https://bitbucket.org/gds/coq-breakpoints
Как некоторые знают, я некоторое время занимаюсь способами привнести немного runtime type information в окамловские строго- и статически- типизированные программы.
Репка -- https://bitbucket.org/gds/cadastr/src
Как один из примеров:
Read more... )
Хочу навести порядок в голове про continuations. То есть, сам принцип базовых continuations я понимаю, callcc (? штука, вводящая "точку возврата"?) тоже понимаю, но не до конца. А вот shift/reset и йоже с ним -- ой как-то нет. Что почитать из тупых книжек, рассчитанных на дебилов? Желательно, конечно, статически-типизированные случаи.

lcm 6 7.2

Oct. 25th, 2011 12:35 pm
Исходный вопрос: [personal profile] nicka_startcev: Какое наименьшее общее кратное у 6 и 7.2 ?
Реализация на C++, обсуждение double: [profile] udpn: Дробная арифметика
Реализация на OCaml, чисто для разминки/отвлечения:
Read more... )
$ ./main.byte
(lcm 6 36/5) = 36


Репка тут.
Всё хорошее, что я говорил про гуй убунты по умолчанию, относилось к релизам <=10.10 и было следствием использования гнома2 в качестве "окружения рабочего стола" в тех версиях. Обновление до 11.04 принесло unity (правда, глючную, но, по слухам, кое-как исправленную в 11.10). Что принесёт обновление до 11.10 -- посмотрим в ближайшее время.
Подумалась такая штука. Если бы я писал на окамле библиотеку типа json-wheel, но для bson или подобных штук, я бы сразу отрефакторил отдельно создание значений: налепил бы модуль, содержащий тип и функции для построения значений этого типа, и из парсера вызывал бы функции этого модуля. Смысл этого таков: потом, если профайлер скажет, что строить в памяти значение и потом "разрушать" его не слишком эффективно, можно будет лёгким движением препроцессора превратить код парсера в функтор, берущий на вход этот самый модуль с типом и функциями для его создания, и -- вплоть до того, что вообще создавать значение с типом unit, работая в стиле xml sax парсера на сайд-эффектах.

upd1/
Производительность при выделении функций, создающих значения этого типа, не меньше, так как они должны будут заинлайниться (когда модуль статический, известный и не функтор). А вот с разрушением значения, представляющего bson в памяти, с целью генерации bson -- сложнее. Понятно, что в общем случае это будет анаморфизм, но как сделать в частном случае, эффективно и с отсутствием оверхеда в случае, когда работа идёт с "родным" типом -- не знаю пока точно (настолько же точно, как про создание значения). Сообщите, если будут идеи (можно в чятик).
komar справедливо заметил некоторое различие в способах вызова окамловских List.fold_{left,right}. Мне тоже это не нравится. Попробуем это решить с максимальным количеством ональных извращений. Ну, чисто на всякий случай. Проверить свою силу, так сказать. Конечно, я -- сугубо против такого кода, сообщу сразу, в качестве дисклизмера. Несмотря на это, буду лелеять своего внутреннего индуса на специально отведённой территории.
Read more... )
# do_with_foldl fold_left;
res=>abc
- : unit = ()

# do_with_foldl (r2l fold_right);
res=>cba
- : unit = ()

# 
Никита Калинин интересуется, $subj
Ответ: ничего. Объяснение отрефакторено из жаббера:

Пост Никиты про CS видел. Думал даже, что именно посоветовать. Но не знаю. Ну вообще.
Read more... )
Неоднозначно это.
(основано на приватной дискуссии в жаббере, слегка отредактировано, просто цитата)

[...] по моему опыту писания на жс там явно не хватает таких вещей:
1. модульность (криво через объекты я умею, нахуй-нахуй),
2. хотя бы тупых вариантных типов данных (через объекты умею),
3. хоть какой-нибудь типизации,
4. closures кривы -- примеры были обсуждены, for (my $i ...), хоть и обходы есть,
5. tail-recursion elimination -- тоже представляю вполне, как это сэмулировать, но в пределах жс общий подход не опишешь, а частные -- уродливы.
Давно хотел вербализовать эту идею, да всё случая не было.
Нас спрашивают: "откуда возник ритуал, запрещающий ставить пустые бутылки на стол?".
Мы отвечаем. Это сродни индексированию в реляционных базах данных, где значения NULL не включаются в индекс по этим значениям. То есть, выборка "table.field = some_value" может использовать этот индекс (так как условие является всегда ложным, если some_value это NULL). Иногда даже специально делают индексы по избранным строкам, делая индекс по функции, принимающей значение NULL на неинтересных строках. Был обрадован, когда узнал, что в постгресе это не нужно, и у индекса есть своя where-часть.
Так вот, когда человек думает "винца, что ли, наебнуть?", он кагбэ выполняет " select * from table where bottle_contents='wine' " (заметьте ещё одну параллель -- table и там, и тут).
Ну и вот скажите, не проще ли заранее убрать из выборки те бутылки, в которых bottle_contents явно не удовлетворит никакому разумному выбору? Проводя нехитрый изоморфизм, наливать из бутылки не захочется только в том случае, если её bottle_contents равно NULL.
Потому и убирают из индекса.
Так-то!
Давняя-древняя мечта о роликах таки реализована с материальной стороны. Осталось тушку и дух подтянуть.
В Одессе гораздо больше выбор роликов, в одном только бутике -- в 5 раз больше, чем во всех Бандёрах. Это не новость и не опускалово какое, это "последняя капля". "Здесь и сейчас", потому что иначе -- либо "потом и говно", либо "потом и гемор".
Ну и адекватный продавец, подсказавший кое-какие слишком уж базовые штуки. Про защиту он подтвердил мои догадки -- "те, кто покупает ролики и не покупает защиту, обычно приходят через 2..3 недели за ней".
Итак, аж целых 106$ за приличные китайские ролики и защиту.
Дальше -- лёгкий rtfm в интернетах, и первые упражнения у меня в руках.
Это было вчера. Сегодня же впервые нормально попробовал попользовать ролики.
В первую очередь научился кое-как вставать с пола. Во вторую очередь -- хорошо и качественно падать. Весь цимес в том, чтобы строго вперёд падать. Для этого -- и центр тяжести вперде, и руки желательно держать локтями вниз в первое время, и стараться согнуть ноги в коленях, чтобы на колени упасть. Ибо на хребет/затылок падать -- хуже некуда. На бок либо с распростёртыми конечностями -- просто плохо. А так -- около 5 раз падал сознательно, какое-то новое ощущение от падения. Всё слишком быстро: раз -- и уже на земле. Тут отреагировать (включить моск, сделать движение) сложно, почти невозможно. Надежда на 1. прошивку, 2. тренировку.

Из рабочих моментов -- жопой чуял, но и практикой подтвердилось, что json-static не умеет параметризованные типы. Понятно, что какой-нибудь option 'a он, ясное дело, парсить и не должен, но 1. он не любит типовые параметры даже в случаях фантомных типов и в случае известных типовых параметров, 2. не умеет генерить json по известному параметризованному типу. Пичалька, но попробуем функторы тут. Но, думается, изначально надо было бы делать (не мне, понятно) что-то типа atdgen, но по технологии deriving'а. С другой стороны, atdgen у меня в планах точно, но попозже.
Все разумные люди знают, что уборка квартиры сама по себе не нужна.
Вещи по квартире рассасываются сами так, как надо, как удобно, как бы выполняя профайлинг доступа к ним методом монтэкарлы.
У меня было даже до состояния самозарождения такой "живности", как "перекати-пол" (так!) из кошачьей шерсти.
Однако, тем не менее, если поддержание чистоты зачем-то нужно (например, просто приятно глазу), есть приём. Не помню, где вычитал, но где-то в жыжыцэ.
Квартира делится на "зоны", уборка которых занимает не больше 15 минут (одна из зон -- пропылесосить ковро, другая -- помыть немного посуды, третья -- помыть пол в коридоре), и вот, во время перерыва между сеансами мысленной деятельности вполне можно заняться чем-то, что не занимает моск, способствует отдыху, но -- чётко контролируемое время, не больше. Главное тут не отключить моск напрочь и не заработаться, иначе физическая усталость, чувство потраченного зря времени и отвращение к процессу. Вплоть до того, что можно будильник заводить, как я периодически делаю, работая по схеме "20 минут работы + 10 минут отдыха" -- ну, типа, "помидорки". (кстати, оказалось, по такой схеме я могу работать порядка 16 часов без перерыва на сон. Потом, правда, отходняк пару дней).
А ещё можно воспользоваться приёмами "автофокуса" -- бытовуху записать на бумажку, на видное место её, и, когда есть настроение, пробежаться глазами по ней, выбрать нужное дело, зачёркивать его наполовину (в случае, если дело периодическое -- дописывать снизу бумажки сразу же, чтобы не потерять его), и идти делать это дело. Дозачеркнуть по исполнении, опционально дописать снизу новые обнаруженные дела. Заодно, в качестве контроля за относительной периодичностью дел -- стараться выбирать дела откуда-то с начала списка. Заодно, в качестве "результата своей деятельности" будете видеть бумажки с полностью зачёркнутыми делами.
Так-то!
Понял, что большинство моих проёбов и лишних затрат времени вызваны откровенно хуёвым планированием. Проанализировав частные случаи, пришёл к выводу, что мне нужны 3 штуки.
Read more... )
Так-то. Однако увязать это воедино -- не знаю, как. Всё сложно. А это говорит о том, что такая система будет либо неудобной, либо нестройной, либо сложной в использовании.
У меня была необходимость разобрать записи, получаемые от реляционки (от постгреса в моём случае), в окамле, который строго типизирован.
Read more... )
Придумалось новое "правило карликов".
(9:16:26) Ivanych: Мне очень так видится, что можно сделать backend для базок данных.
И одновременно, язычок-backend.
(9:22:18) gdsfh: про backend -- не знаю, просто данные сложить можно, и даже не ёбаный пиздец [в плане сложности реализации], но 1. дубовая структура "таблицы->строки->столбцы" -- фи. 2. транзакции делать -- гемор адский.
(9:22:48) Ivanych: Естественно, что этот быкенд должен поддерживать не только таблички.
(9:29:29) Ivanych: Конечно не такая дубовая структура!
Надо сделать, чтобы в каждом row могли быть разные типы!
(9:29:58) gdsfh1: лололо
(9:30:13) Ivanych: И разное их количество и типы разные, да!
(9:31:28) gdsfh1: беспорядочно содомирующие друг друга!
(9:31:39) Ivanych: ;-) ;-) Exactly!

Правило проверено пока только эмпирически и имеет нестрогий вид: "Если про элементы сложной системы можно сказать 'бегающие по арене и беспорядочно содомирующие друг друга', то, вероятно, система является либо переусложнённой (overengineered), либо логически нестройной, либо слишком расслабленной в плане получаемых от неё гарантий".
Новая дисциплина в функциональном программировании: художественный карринг. Программист подстраивает порядок аргументов так, чтобы частичные применения различного числа аргументов к функции покрывали все или почти все случаи её использования.
Разгрыз аппликативные функторы. Лучше поздно, чем никогда. И не просто в теории, но и на практике тоже.
Хорошая штука для своих применений, главное из которых -- эмуляция "функции с переменным количеством аргументов".
В моём конкретном примере, имея некое окружение (заданное статически пока что, в виде [("a", String "str"); ("b", Int 123); ("c", Bool True)]), код

value () = run &
  (fun f -> f <$> string "a" <*> int "b" <*> bool "c")
  (Printf.printf "a=%S b=%i c=%b")
;


выводит ожидаемое:
a="str" b=123 c=true


Мне эти функторы пригодятся для обработки значений с типом sql_t = [ `Null | `String of string | `Binary of string | ... ].

Конкретику ищите в репке "amall", если представляете, что это.

overbld

May. 10th, 2011 12:19 pm
Писал в жаббер, но понял, что тут этому тоже место. Рассматриваем вопрос "overbld -- хорошо или плохо?".

В случае ебилдов/портов/пакетов ответственность за безглючность и свежесть ложится на мейнтейнеров, причём по принципу "and": чтобы твоя софтина компилялась на gentoo, freebsd, debian, ubuntu, redhate, suse, все мейнтейнеры всех операционок обязаны предоставить пакеты, дающие не самую старую версию всех используемых библиотек/инструментов.
Если бы был коммунизм, в котором была бы Единая ОС (ну, там, Единая Нация и Единый Вождь уже как бы подразумеваются), то я бы не стал лепить горбатого оверблда. А так -- я лично отвечаю за обновления, безглючность, компилируемость, и у меня это получается лучше, чем у связки "багтрекер каждого дистра + группа мейнтейнеров каждого дистра + каждый дистр со своими версиями/патчами + апстрим библиотек/утилит".
Уже долго прикидываю так и эдак, но не могу до конца сообразить.
Есть мой dumbstreaming -- протокол для передачи строк, который планирую расширить так, чтобы он позволял передавать не одну строку в одном пакете, а несколько строк сразу.
Конечно, я изобретаю tnetstrings, но у меня преимущество: типы известны заранее (а именно, строки), а не указываются в конце сообщения, сразу известно количество и объём каждой строки, ну и разделители помогают надёжности. Эти преимущества позволят обрабатывать всё потоковым образом.
Для этого у меня есть iteratees.
Задача парсинга разбивается явно на два слоя: 1. парсер потока, которым передаются списки строк, работа с длинами и количествами строк, разделителями -- собственно, дело библиотеки, и 2. парсер непосредственно строк, для каждой строки в теории свой итерат.
Пока единственное, что получилось, это
value read : (stringscount:int -> list (iteratee char 'a)) -> iteratee char (list 'a)
То есть, пользовательская функция получает количество строк в пакете и возвращает список результатов.
Ещё есть идейки позаигрывать с fold:
value read : (stringscount:int -> 'a -> iteratee char 'a) -> 'a -> iteratee char 'a
-- функция получает количество строк в пакете (на всякий случай), текущее значение аккумулятора и возвращает итерат, который будет применён к потоку и который возвратит следующий аккумулятор для следующей строки в пакете.
Однако, весь цимес итератов как раз состоит в замене fold для ввода-вывода. То есть, жопой чувствую, тут может получиться всё решить вложенными(?) итератами. Но как -- не могу сообразить. В общем, простой bind итератов меня бы устроил, было бы (it1 >>= fun v1 -> it2 >>= fun v2 -> return v1 + v2), но фишка в том, что it1 и it2 должны не трогать поток за пределами того, что им выделено, то есть, если в терминах итератов, должно было бы быть что-то типа ((join & take len1 it1) >>= fun v1 -> (join & take len2 it2) >>= fun v2 -> return v1 + v2), и не представляю, как это сделать.
После того, как описал, чуть-чуть прояснился вопрос (а именно, попробовать пойти так же, как из fold получились итераты первого уровня), но, всё равно, как-то непонятно.

UPD2.
"Давай по-новой, Миша, все хуйня."

value read : (ntotal -> npart -> nbytes -> iteratee char 'i)
          -> iteratee 'i 'a
          -> iteratee char 'a

первый аргумент -- пользовательская функция, на основании количества кусков, номера куска и количества байтов в куске выдающая итерат, который будет кушать байтики этого куска и возвращать значение с типом 'i. Второй аргумент -- итерат, который будет кушать значения с типом 'i и возвращать результат с типом 'a. И функция read родит итерат, который применяем к потоку байтов и имеем результат с типом 'a.
Почему преобразование 'i -> 'a и почему не возврат list 'i? Потому что это простым образом делается из текущей схемы, передавая стандартный итерат stream2list, который как раз iteratee 'i (list 'i).
В камлочятике жалуются на asp.net. Ну да, говно как говно, но в аромате чувствуется запах любимой копрорации. Поначалу писалось в чятик, но потом оформилось сюда.

Я же, наоборот, себя периодически заставляю сделать что-нибудь эдакое. Потому что к хорошему привыкают. То на сишечьке что-нибудь асилю, то, вон, по говнокодерским методам расчёт длин хорд для точек, равномерно расположенных на окружности, сделал вчера, чисто для практических штук: моя леди поделилась задачей, нужной для прикольной штуки -- цветочки делать из ниток, но там, если делать тупо, с погрешностями не здорово, поэтому и нужно посчитать.

А говнокодерские методы, кстати, отдельная история. Вплоть до поиска "javascript function definition" для определения функции -- ну забыл, реально.

Есть иногда такая штука, когда хочется взять отдельную задачу и решить её, не отрываясь на что-либо другое. Марш-бросок, что ли. Такое канает в случае задач, решаемых весьма быстро, и гораздо меньше канает в случае подзадач, хоть и решаемых быстро, но не имеющих практического выхлопа прямо здесь и сейчас.
Page generated May. 23rd, 2017 04:55 pm
Powered by Dreamwidth Studios