Зарелизил мелкую библиотечку для отладки редукций выражений в пределах coq: https://bitbucket.org/gds/coq-breakpoints
Как некоторые знают, я некоторое время занимаюсь способами привнести немного runtime type information в окамловские строго- и статически- типизированные программы.
Репка -- https://bitbucket.org/gds/cadastr/src
Как один из примеров:
Read more... )
Хочу навести порядок в голове про continuations. То есть, сам принцип базовых continuations я понимаю, callcc (? штука, вводящая "точку возврата"?) тоже понимаю, но не до конца. А вот shift/reset и йоже с ним -- ой как-то нет. Что почитать из тупых книжек, рассчитанных на дебилов? Желательно, конечно, статически-типизированные случаи.
komar справедливо заметил некоторое различие в способах вызова окамловских List.fold_{left,right}. Мне тоже это не нравится. Попробуем это решить с максимальным количеством ональных извращений. Ну, чисто на всякий случай. Проверить свою силу, так сказать. Конечно, я -- сугубо против такого кода, сообщу сразу, в качестве дисклизмера. Несмотря на это, буду лелеять своего внутреннего индуса на специально отведённой территории.
Read more... )
# do_with_foldl fold_left;
res=>abc
- : unit = ()

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

# 
Просто вялые размышления о динамической типизации и зависимых типах.

подумал, что языки с динамической типизацией -- это как бы "языки с зависимыми типами". например,
function add(a, b) { return (a + b); };

вполне можно записать как
add : Ta : Type -> a : Ta -> Tb : Type -> b : Tb -> Ta =
if Ta = Number
then add_number a (cast_to_number Tb b)
else if Ta = String
then concat a (cast_to_string Tb b)
else fail

, в случаях, когда определены
cast_to_number : T : Type -> x : T -> number
cast_to_string : T : Type -> x : T -> string

Фактически, любое значение имеет ассоциированный с ним в рантайме тип, и можно было бы в примере выше передавать сразу (Ta : Type, a : Ta) в виде туплов.
Однако, если с add было понятно, что вернётся значение с типом Ta, то в случае неизвестного типа будет возвращён именно тупл (T:Type, x:T), но не простой, а с проставленными ограничениями (именно: второй компонент имеет тип, равный первому компоненту). А как такое рассматривать -- пока не знаю. Кто-нибудь ковырял языки с зависимыми типами? Должен быть, по идее, штатный подход.
Никита Калинин интересуется, $subj
Ответ: ничего. Объяснение отрефакторено из жаббера:

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

[...] по моему опыту писания на жс там явно не хватает таких вещей:
1. модульность (криво через объекты я умею, нахуй-нахуй),
2. хотя бы тупых вариантных типов данных (через объекты умею),
3. хоть какой-нибудь типизации,
4. closures кривы -- примеры были обсуждены, for (my $i ...), хоть и обходы есть,
5. tail-recursion elimination -- тоже представляю вполне, как это сэмулировать, но в пределах жс общий подход не опишешь, а частные -- уродливы.
У меня была необходимость разобрать записи, получаемые от реляционки (от постгреса в моём случае), в окамле, который строго типизирован.
Read more... )
Разгрыз аппликативные функторы. Лучше поздно, чем никогда. И не просто в теории, но и на практике тоже.
Хорошая штука для своих применений, главное из которых -- эмуляция "функции с переменным количеством аргументов".
В моём конкретном примере, имея некое окружение (заданное статически пока что, в виде [("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).
а у меня -- интересное. Впрочем, вытекающее из стиля разработки парвела. Захотел параллельно-запускающиеся процессы с ограничением количества -> захотел следить за выходящими процессами тоже, не только за "серверами" -> понадобилось что-то типа эрланговского monitor -> (куча сломанных/изменённых типов) -> понадобилось сообщение процессам типа `Exited of что-то and process_exit_status -> понадобилась обработка сообщения другими, уже написанными процессами-серверами, причём кое-где даже сознательная, например в "диспетчере", который по ключу и соответствиям "ключ => процесс" определяет, кому отправить сообщение -> понадобилось вычёркивать процессы, чей ключ ничему более не соответствует -> понадобилось идентифицировать процессы -> понадобился pid. Вот так. Статическая типизация заставила меня ввести пиды, хочу я того или не хочу.
Предупреждение: вопрос глупый. Слабонервным не читать.

Мы с коллегой проектируем протокол общения двух программ. Общение состоит в том, что одна программа пишет в stdin/пайп/сокет для другой программы сообщение, являющееся валидным json (в строгом смысле слова -- либо массив, либо объект, то есть, self-delimited), другая программа читает, обрабатывает и отсылает ответ обратно, тоже json.
Запросов и ответов может быть много в одном потоке, они идут последовательно, на каждый запрос один ответ. И есть варианты, как это всё писать в один сплошной поток байтов.

1. Писать как есть, а парсер json'а разберётся, где заканчивается массив-объект (тупым подсчётом скобочек, исключая содержимое строк, например; либо средствами json-парсера),
2. Генерировать json так, чтобы он не содержал пустых строк (последовательности байтов 0x0A 0x0A), писать его в поток и разделять разные сообщения пустой строкой,
3. Писать сначала длину сообщения в байтах в десятичном представлении, затем перевод строки, затем само сообщение, содержащее ровно указанное количество байт.
4. Взять протокол наподобие http, имеющий возможность как слать сообщения с указанной длиной, так и сообщения в чанках, так и сообщения "до закрытия канала".

(соответственно, конец общения различать в соответствующих случаях так: 1. просто закрытый на отсылку поток (eof), 2. eof либо пустая строка вместо json, 3. eof либо сообщение длиной 0, 4. закрытие канала по канонам rfc2616.)

У нас возникли разногласия о том, как же это сделать, и я решил узнать общественное мнение.
Какой бы формат выбрали вы?

За какой вариант я и за какой вариант коллега -- не скажу пока. В качестве бонуса можете попробовать это угадать, а я через пару дней расколюсь.

MapM

Apr. 18th, 2011 11:20 am
Abstract:
В данной статье я расскажу вам про отображающие функции вида map, включающие в себя сайд-эффекты. Тем, кому известен хаскель, эти функции известны как mapM и подобные.
Далее, будет показано, что хаскель, будучи самым распространённым языком из тех, где используются монады (ну, кроме C#/linq и Scala), является непрактичным из-за отсутствия сайд-эффектов. Раньше мне без сайд-эффектов было всего лишь просто неудобно использовать хаскель (требовалось городить лишний код), теперь же я понимаю, что есть некоторые вещи, где с чистотой не получится клёво использовать монады в одном из их применений.
Также будет показано, что тайпклассы -- это не гибко, потому что у одного тайпкласса и у одной функции (например, "функция sequence в монаде IO") может быть только одна реализация, и будет показано, где именно это не гибко.

Read more... )

Кроме того, видел сегодня клёвую статью Modules Matter Most. Она тут упомянута потому, что в ней тоже необоснованно гонят на хаскель, но сама статья хорошая и правильная.
Page generated Jun. 27th, 2017 08:43 pm
Powered by Dreamwidth Studios