gdsfh

Зарелизил мелкую библиотечку для отладки редукций выражений в пределах coq: https://bitbucket.org/gds/coq-breakpoints

Хочу навести порядок в голове про continuations. То есть, сам принцип базовых continuations я понимаю, callcc (? штука, вводящая "точку возврата"?) тоже понимаю, но не до конца. А вот shift/reset и йоже с ним -- ой как-то нет. Что почитать из тупых книжек, рассчитанных на дебилов? Желательно, конечно, статически-типизированные случаи.

Всё хорошее, что я говорил про гуй убунты по умолчанию, относилось к релизам <=10.10 и было следствием использования гнома2 в качестве "окружения рабочего стола" в тех версиях. Обновление до 11.04 принесло unity (правда, глючную, но, по слухам, кое-как исправленную в 11.10). Что принесёт обновление до 11.10 -- посмотрим в ближайшее время.

komar справедливо заметил некоторое различие в способах вызова окамловских List.fold_{left,right}. Мне тоже это не нравится. Попробуем это решить с максимальным количеством ональных извращений. Ну, чисто на всякий случай. Проверить свою силу, так сказать. Конечно, я -- сугубо против такого кода, сообщу сразу, в качестве дисклизмера. Несмотря на это, буду лелеять своего внутреннего индуса на специально отведённой территории.
( Read more... )

# do_with_foldl fold_left;
res=>abc
- : unit = ()

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

# 

(основано на приватной дискуссии в жаббере, слегка отредактировано, просто цитата)

[...] по моему опыту писания на жс там явно не хватает таких вещей:
1. модульность (криво через объекты я умею, нахуй-нахуй),
2. хотя бы тупых вариантных типов данных (через объекты умею),
3. хоть какой-нибудь типизации,
4. closures кривы -- примеры были обсуждены, for (my $i ...), хоть и обходы есть,
5. tail-recursion elimination -- тоже представляю вполне, как это сэмулировать, но в пределах жс общий подход не опишешь, а частные -- уродливы.

Давняя-древняя мечта о роликах таки реализована с материальной стороны. Осталось тушку и дух подтянуть.
В Одессе гораздо больше выбор роликов, в одном только бутике -- в 5 раз больше, чем во всех Бандёрах. Это не новость и не опускалово какое, это "последняя капля". "Здесь и сейчас", потому что иначе -- либо "потом и говно", либо "потом и гемор".
Ну и адекватный продавец, подсказавший кое-какие слишком уж базовые штуки. Про защиту он подтвердил мои догадки -- "те, кто покупает ролики и не покупает защиту, обычно приходят через 2..3 недели за ней".
Итак, аж целых 106$ за приличные китайские ролики и защиту.
Дальше -- лёгкий rtfm в интернетах, и первые упражнения у меня в руках.
Это было вчера. Сегодня же впервые нормально попробовал попользовать ролики.
В первую очередь научился кое-как вставать с пола. Во вторую очередь -- хорошо и качественно падать. Весь цимес в том, чтобы строго вперёд падать. Для этого -- и центр тяжести вперде, и руки желательно держать локтями вниз в первое время, и стараться согнуть ноги в коленях, чтобы на колени упасть. Ибо на хребет/затылок падать -- хуже некуда. На бок либо с распростёртыми конечностями -- просто плохо. А так -- около 5 раз падал сознательно, какое-то новое ощущение от падения. Всё слишком быстро: раз -- и уже на земле. Тут отреагировать (включить моск, сделать движение) сложно, почти невозможно. Надежда на 1. прошивку, 2. тренировку.

Из рабочих моментов -- жопой чуял, но и практикой подтвердилось, что json-static не умеет параметризованные типы. Понятно, что какой-нибудь option 'a он, ясное дело, парсить и не должен, но 1. он не любит типовые параметры даже в случаях фантомных типов и в случае известных типовых параметров, 2. не умеет генерить json по известному параметризованному типу. Пичалька, но попробуем функторы тут. Но, думается, изначально надо было бы делать (не мне, понятно) что-то типа atdgen, но по технологии deriving'а. С другой стороны, atdgen у меня в планах точно, но попозже.

Понял, что большинство моих проёбов и лишних затрат времени вызваны откровенно хуёвым планированием. Проанализировав частные случаи, пришёл к выводу, что мне нужны 3 штуки.
( 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", если представляете, что это.

Уже долго прикидываю так и эдак, но не могу до конца сообразить.
Есть мой 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).