Зарелизил мелкую библиотечку для отладки редукций выражений в пределах 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


Репка тут.
Подумалась такая штука. Если бы я писал на окамле библиотеку типа json-wheel, но для bson или подобных штук, я бы сразу отрефакторил отдельно создание значений: налепил бы модуль, содержащий тип и функции для построения значений этого типа, и из парсера вызывал бы функции этого модуля. Смысл этого таков: потом, если профайлер скажет, что строить в памяти значение и потом "разрушать" его не слишком эффективно, можно будет лёгким движением препроцессора превратить код парсера в функтор, берущий на вход этот самый модуль с типом и функциями для его создания, и -- вплоть до того, что вообще создавать значение с типом unit, работая в стиле xml sax парсера на сайд-эффектах.

upd1/
Производительность при выделении функций, создающих значения этого типа, не меньше, так как они должны будут заинлайниться (когда модуль статический, известный и не функтор). А вот с разрушением значения, представляющего bson в памяти, с целью генерации bson -- сложнее. Понятно, что в общем случае это будет анаморфизм, но как сделать в частном случае, эффективно и с отсутствием оверхеда в случае, когда работа идёт с "родным" типом -- не знаю пока точно (настолько же точно, как про создание значения). Сообщите, если будут идеи (можно в чятик).
Просто вялые размышления о динамической типизации и зависимых типах.

подумал, что языки с динамической типизацией -- это как бы "языки с зависимыми типами". например,
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... )
Неоднозначно это.
У меня была необходимость разобрать записи, получаемые от реляционки (от постгреса в моём случае), в окамле, который строго типизирован.
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).
Кто там объекты-классы-методы не любит? Покритикуйте и предложите вариант получше:
Read more... )
я тут кратенько изложил концепции парвела, чтобы перед глозаме была общая картина того, что же я делаю. https://bitbucket.org/gds/parvel/wiki/concepts_rus
а у меня -- интересное. Впрочем, вытекающее из стиля разработки парвела. Захотел параллельно-запускающиеся процессы с ограничением количества -> захотел следить за выходящими процессами тоже, не только за "серверами" -> понадобилось что-то типа эрланговского monitor -> (куча сломанных/изменённых типов) -> понадобилось сообщение процессам типа `Exited of что-то and process_exit_status -> понадобилась обработка сообщения другими, уже написанными процессами-серверами, причём кое-где даже сознательная, например в "диспетчере", который по ключу и соответствиям "ключ => процесс" определяет, кому отправить сообщение -> понадобилось вычёркивать процессы, чей ключ ничему более не соответствует -> понадобилось идентифицировать процессы -> понадобился pid. Вот так. Статическая типизация заставила меня ввести пиды, хочу я того или не хочу.

MapM

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

Read more... )

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