gdsfh

Делаю вот одну шнягу на окамле. Там есть файл, в нём "блоки данных", состоящие из подблоков малой длины.
И подумал я, что дёргать каждый раз Unix.read (обёртку над read()) не очень гуманно в плане количества вызовов ОС, например.
И решил я реализовать более умный алгоритм чтения-кеширования, читающий в блок размера "дисковый блок * 2", по выравненным смещениям, стараясь читать по границе блока, чтобы не читать ненужные блоки. Однако, кое-где явно нет нужды пропускать данные через буфер, когда ясно, что "цельные блоки" можно прочитать напрямую в строку-получателя.
Но оказалось, что я не смог отладить этот сугубо императивный алгоритм руками, и у меня вообще не было уверенности в том, что он работает правильно. Эти гадские смещения, длины! Невозможно интуитивно проверить, правильно ли сделал. Очень БЕСЕД, знаете ли.

Тогда я взял Coq.
( Read more... )

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

Сегодня lj\thedeemon показал ужосы, от которых у меня волосы в жилах стынут.
А мне стало интересно, можно ли накосячить подобным образом в coq.
Но писал я быстро, поэтому код некрасивый. Например, можно спокойно попрятать многое в implicit arguments, да и для vec выбрать более кошерный тип (например, кошерный в плане strict positivity).

( Read more... )

Однако, кое-какая лажа у меня таки была. Если rewrite, ныне вынесенный в vec_cast, натравить не на чистый пруф-терм ("n = m -> length l = n -> length l = m"), а на computational term (в том числе содержащий пруф) ("n = m -> vec A n -> vec A m"), то Eval compute выдаёт совершенно аццкий терм, содержащий в том числе пруф того, что длины равны. Но в #coq быстро объяснили, в чём дело. В этом состоит мой личный профит от этой задачки. Ну и развлёкся, и убедился, что в coq подобные косяки допустить трудно, даже если используются тактики.

Есть время собирать опыт.

Есть время разбрасывать на вентилятор.

Уже довольно давно система типизации в окамле кажется мне слегка недостаточной.
( Read more... )

По итогу -- впечатления смешанные.

Интересно просуммировать, что же я сделал за год. (дата выбрана совершенно случайно, но "новый год" выбирать как-то неоригинально.) Не упорядочено никак. И не пишу, благодаря кому это делал -- слишком многих перечислять придётся.
( Read more... )

upd1/
( Read more... )

upd2/
( Read more... )

upd3/
( Read more... )

Обсуждали изготовление домашнего кваса, опубликую личный рецепт.
( Read more... )

(как бы разворачивая каменты из предыдущего поста)

А расскажите, где вообще полезны dependent types?
Про примеры с массивами и их границами я в курсе, но это мало полезно лично мне на практике -- дело в том, что я как-то не нарывался на проблемы с этим уже несколько лет, причём dependent types не использовал для этого никак, ни разу. (а вот модульность и нормальные интерфейсы модулей -- как раз использовал.)
Далее, понятно, с помощью dependent types можно протаскивать какие-то утверждения в compile time. Очень хорошо, но с какими практическими целями?
Что я уже читал: первые несколько страниц выдачи гугла по "dependent types", в том числе известное "why dependent types matter". И, всё равно, либо dependent types это малонужная хуйня, либо я тупой. (не стесняйтесь, я прекрасно знаю свои интеллектуальные способности, поэтому последний вариант не оскорбителен.)

Data.VecN в окамле: https://bitbucket.org/gds/vecn/src
И, чорт возми, опять зависимые типы не пригодились. Да что за беда...

как из пизды на лыжах, появился на пстачике. политика -- http://gds.psto.net/oiifii , бложек -- http://gds.psto.net/ , фид -- http://gds.psto.net/rss

upd/
остальные бложеки будут использоваться в прежнем режиме. может чуть меньше хуиты там будет, разве что.

upd2/
как на меня подписаться жаббером: 1. добавляете в контакт-лист psto@psto.net , 2. выбираете незанятый юзернейм, отправляете команду "register юзернейм", 3. подтверждаете регистрацию, 4. отправляете команду "S @gds".

да, регистрация -- это уныло. но пока зерт не допилил metalkia.com, буду срать в пстачик.

Одна из частей моего интернет-общения с людьми состоит в том, что я шлю одинаковые/похожие сообщения по жабберу нескольким людям одновременно.
По идее, для автоматизации этого процесса нужен блог/микроблог (тьфуты, пойду помою язык) с поддержкой возможности постить через жаббер и с возможностью людей "подписаться" (так, чтобы им в жаббер приходили мои "посты").
Вот его и попытаюсь найти, а вы, читающие этот пост, может быть подскажете, что мне подойдёт. Вдруг сталкивались или слышали о подобном.
Сразу скажу, что твитор и жуйк мне не подходят, по разным, но весьма серьёзным причинам, их давайте откинем, даже если они удовлетворяют описанным мной требованиям.
От подобного сервиса очень желательно иметь возможность видеть в вебморде эти "посты", хотя бы чтобы можно было на них сослаться http-ссылкой, ну и для любителей эфпячить вместо более культурных средств. Ещё очень хочется rss/atom и подобное, для тех, кто предпочитает не реалтайм-доставку жаббером, а чтение фидов.
Это -- минимальные требования к сервису. Больше и не нужно. Всякие каменты -- хрен его знает, нужны ли. Будут -- хорошо, не будут -- проживу.
Подскажите, есть ли в интернетах бесплатный сервис, предоставляющий подобную функциональность?

Меня давно волнует это тема, но в последнее время появилась явная практическая необходимость в ней, поэтому от личного и полупубличного обдумывания перейду к публичному.

Хочется мне построить одну систему в идеологии actors (или близкой к ней).
( Read more... )

Как некоторые знают, я некоторое время занимаюсь способами привнести немного runtime type information в окамловские строго- и статически- типизированные программы.
Репка -- https://bitbucket.org/gds/cadastr/src
Как один из примеров:
( Read more... )

Нас спрашивают:

А вы можете придумать такую нетрансцендентную метрику, чтоб пи в ней стабильно было равно трём? не четырём, не два корня из двух, а именно ровно трём.

А вот однако можем, но, видимо, это случайность.
Точнее, тут надо придумывать не метрику, а целую топологию и геометрию.
Этим требованиям удовлетворяет дискретное топологическое пространство, представленное вершинами равносторонних треугольников, плотно и без перекрытий заполняющих двумерную плоскость R².
Как я понимаю, это определяет топологическое пространство вполне, кроме того, можно ввести геометрические сущности: расстояние будем считать по минимальному количеству шагов между точками (и обычно таких путей много, но есть набор минимальных).
Окружность радиуса 1 (диаметра 2) будет представлена шестиугольником со стороной 1. Окружность радиуса n (диаметра 2n) будет представлена шестиугольником со стороной n.
Таким образом, периметр шестиугольника, представляющего окружность диаметра 2n, будет равен 6n, а число π будет равно 6n/2n = 3.
Так-то!

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

Исходный вопрос:

nicka_startcev: Какое наименьшее общее кратное у 6 и 7.2 ?
Реализация на C++, обсуждение double:

udpn: Дробная арифметика
Реализация на OCaml, чисто для разминки/отвлечения:
( Read more... )

$ ./main.byte
(lcm 6 36/5) = 36

Репка тут.

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

Я это рассказывал и раньше, но как-то в реаллайфе, не письменно. Опишу же.
Помнится, где-то в 2006..2007г мне довелось порядка года снимать квартиру в одном районе города, который как бы почти ебеня, но индустриальные (там даже почти пол-района на ул.Индустриальной находится), и какой-то неблагополучный район сам по себе. Но и даже в этом районе была своя звезда -- тот самый дом, где я снимал квартиру. Он отличался наличием около трёх лавочек, где собирался цвет общества. Когда часов в 6 выходил на улицу -- они ещё искали бухло. Когда часов в 7 -- они уже бухали. На выходные я выходил на улицу, бывало, в 8..10 часов утра -- они уже готовые. Где-то к полудню собирались по домам, спали несколько часов. К 17..18 часам выходили снова, к 18..19 часам находили бухло (обычно -- спирт, набодяженный с водой до 40 градусов), где-то к вечеру все уже достигали состояния готовальни и шли спать.
То есть, их период был равен 12 часам. Я их назвал "двухтактные".
Но среди них были и трёхтактные индивиды, у которых с двухтактными совпадала утренняя бухашка, а дальше как придётся. Могут же люди!
А потом я съехал в центр и лишился простых радостей жизни, связанных с наблюдением приподъездных алкашей.
Так-то.

Посоны, расскажите про сабж. 1. почему с ним все носятся? 2. что надо слушать, чтобы впирало не по-детски? (наугад выбранные видео с ютуба не впёрли.)

Порицаю "водоканал". Очевидно же, что в системе водоснабжения каждой квартиры должен быть стандартный разъём для подключения пользовательских потребителей воды. (например, шланга, с малой скоростью вливающего воду в аквариум, либо "умной плиты" с возможностью прямо в кастрюлю долить нужное количество воды.) Иначе получается еботня и никакой автоматизации/механизации процессов.

менеджер по залупкам из села Неразлупаловка

Profile

gdsfh

August 2013

S	M	T	W	T	F	S
				1	2	3
4	5	6	7	8	9	10
11	12	13	14	15	16	17
18	19	20	21	22	23	24
25	26	27	28	29	30	31

Syndicate

Page Summary

Style Credit

Style: Neutral Good for Practicality by timeasmymeasure

Expand Cut Tags

No cut tags

Page generated Oct. 17th, 2017 02:46 pm

Recent Entries

(no subject)

coq-breakpoints

построение термов тактиками в coq -- безопасно

Опыт использования Coq на практике, или Как я сам себя отпетушил COQОКОКОКО

год

(no subject)

dependent types

vecN

(no subject)

blog + jabber

actors + пул + протокол

ocaml runtime type information

π = 3

continuations

lcm 6 7.2

ubuntu default gui

двухтактные пассажиры жизни

? death in june

(no subject)

совместное творчество

Profile

August 2013

Syndicate

Most Popular Tags

Page Summary

Style Credit

Expand Cut Tags