Category: it

Category was added automatically. Read all entries about "it".

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

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

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




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

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

вся правда про меня

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

Не тебе судить.
Да, для работы с ленивостью в реальных больших проектах, где условно говоря, много "IO", нужен некоторый опыт. А примеры твои ничего не стоят.
Остальное, в GHC/Haskell, ты откидываешь. И уже вполне приблизился к фанатизму "раз этого нет в любимом инструменте, то это не нужно".
Твои познания за использование ленивости только очень теоретические. Причём, специфической направленности — выискиывать различные fuckup'ы с ленивостью. Вот я тебя спрошу — а приведи примеров хороших и грамотных решений? Ты нормально не ответишь. Зато примеры fuckup'ов привести сможешь.
Ты не разбираешься в теме. Не тебе судить.

(no subject)

ответ на очередное тупопёздничество этой леди, на этот раз тут: http://nicka-startcev.livejournal.com/1651259.html?thread=5538875#t5538875

(кстати, удивлён, что ребе Белнетмон как-то умудрился не хамить открыто.)

> когда меня манагер спрашивает, сколько времени займёт разработка такого-то девайса, я всегда говорю: столько, сколько нужно, плюс время, которое мы тратим сейчас на эту бесполезную болтовню :)

Разработка для разработки. Это так мило. Косвенно напоминает известный анекдот про "откуда деньги берутся? из тумбочки.". Ебануться можно. Налицо тупое непонимание того, что результат работы и сроки готовности результата _напрямую_ влияют на прибыль компании. (Или там такая компания, где делай что хочешь, забивай болт по необходимости, но деньги всё равно будут идти? Даже с заранее увеличенными в несколько раз сроками, определяемыми левой пяткой разработчика? Тогда я бы тоже поработал там, если не совсем нищенская зарплата.)


> чем больше разработчику предоставляется благ - тем эффективнее он работает.

Пока не начинает понимать, что можно и не работать, а прокрастинировать, заниматься хуйнёй, чесать лиловую лысину на рабочем месте, драться саблями (пруф в xkcd). До наступления этого понимания проходит не так уж много времени (если разработчик умный), и тогда у организации начинает медленно подниматься вопрос про то, что и как делать дальше с этой вашей разработкой. Просто увольнять невыполняющего работу сотрудника -- гемор, я читал ТК рашки и приднестрашки. И не надо говорить, что все люди пиздец какие честные, и все просто одержимы тупым кодингом всякой хуйни.

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

А ещё бывает так, что разработчик долбится рогами в совершенно другие ворота, не в те, в которые нужно. Конечно, если дело не в тупых микроконтроллерах, где всё, что нужно от обезьянки-кодера -- это всосать несложную предметную область и хуярить на какой-нибудь сишечььке.
Кроме того, для лучшего результата, бывает, нужно сверху как-то повлиять -- показать более кошерный способ реализации, переосмыслить ТЗ, чуток поменять архитектуру. А если каждому разработчику дать полную свободу от бумажек (в том числе от тех, где он описывает архитектуру, планы и сроки) -- поимеем и хуёвую архитектуру, и кривые×неактуальные планы, и проёбанные сроки. И, в рот тебе ноги, проёбанную прибыль компании. Хотя, опять же, если дело ремесленное -- будь то настраивать проводки в 1С, будь то писать дейтинги и дорвеи на похапэ, будь то лепить тупой говнокод на микроконтроллерах -- вполне можно дать разработчикам швабодку. Проблемы начнутся попозже, в таком случае.

rdbms, global id / hosts

А теперь -- о тупой практике вопрос.
Задаю тут, так как знаю, что по крайней мере четверо из читающих меня людей сталкивались с этой проблемой.
Хочется в пределах реляционной базы данных сделать так, чтобы id записей с разных, но подконтрольных мне баз данных не перекрывали друг друга, и при этом могли генерироваться независимо и локально.
Конечная цель -- создавать такие строки таблиц, чтобы таблицы можно было сливать-разливать по необходимости.
Я знаю только два хака для этого.
1. Прямой хак: сделать так, чтобы первичный ключ записи включал в себя (local_id serial, host_id integer) (вариант -- host_name varchar). Хорошо тем, что индекс по (local_id, host_id) в большинстве случаев (для запросов по локальным данным) будет ровно настолько же селективен, как и просто по local_id. Хотя он будет жирнее, что не радует. Ещё больше не радует то, что соединять таблицы придётся по двум полям, внешние ключи тоже будут по двум полям.
1а. Вариант прямого хака: иметь local_id, host_id, но формировать из них уникальную строку (например, тупо, "123.456" для local_id=123 и host_id=456, или более умно, побитово), которую уже считать идентификатором. Нормально, но первичные/внешние ключи по строковым типам обычно медленнее, чем по numeric типам. И вообще, какое-то сомнительное решение.
2. Кривой хак: закодировать host_id в самом id, например, выделяя какие-то биты (старшие/младшие) под host_id, остальные биты оставляя под local_id. Не нравится тем, что этим сильно ограничивается либо диапазон host_id, либо диапазон local_id, и это потребует проверки со стороны программы (либо ошибки со стороны бд), попадает ли новый локально-сгенерированный id в то множество host_id, в которое он должен попадать. А мне нужно для постгреса, а там самый большой целочисленный тип хранит 8 байт, и не уверен, что их хватит в случае таблиц, с которыми будет вестись интенсивная работа. Кроме того, решение хуже тем, что где-то нужно централизованно выдавать host_id, тогда как решение из п.1 с host_name требует только разумной выдачи host_name, такой, чтобы они не пересекались.

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

(думал поставить на этот пост "тематику только для взрослых", но уже запечатал конверт.)

(no subject)

Я как-то утверждал, что среди хаскеллистов много мудаков. Статистики у меня не было, да и с тех пор с незнакомыми пользователями х-я общался мало. Поэтому будем потихоньку собирать статистику.
(14:01:10) gds: а инфиксные функции вообще усложняют чтение кода.
(15:55:40) klapaucius: "инфиксные функции вообще усложняют чтение кода" Поэтому самый популярный язык программирования - лисп.

опрос: протокол + байты + json

Предупреждение: вопрос глупый. Слабонервным не читать.

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

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

Текущие-бегущие итоги:
Collapse )
трололо

MapM

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

Collapse )

Кроме того, видел сегодня клёвую статью Modules Matter Most. Она тут упомянута потому, что в ней тоже необоснованно гонят на хаскель, но сама статья хорошая и правильная.

парсинг, wtf

Господа, я вот не понимаю такую штуку.
Чтобы задать "регулярный" язык программирования (не ублюдочные в плане синтаксиса и грамматики C/C++), нужно в общем-то очень и очень немного входной информации. Почти нихуя не нужно.
Collapse )
В общем, на эту штуку много времени тратить не хочу принципиально, поэтому спрошу: есть что-нибудь, позволяющее из тупого описания синтаксических конструкций сделать парсер?
А то же придётся самому говнокодить нечто несуразное.

subtyping / подтипизация / ocaml

В окамловском чятике ocaml@conference.jabber.ru dimitrykakadu спросил, что же такое "+'a" в определении типовых параметров. На страницах нашей уютненькой жыжыцы редакция сейчас будет отвечать за базар.
Итак, кратко: +'a означает, что данный параметр ковариантно входит в тип. -'a — соответственно, контрвариантно. Просто 'a — ни так, ни эдак (инвариантно).
Под катом — объяснение подтипизации за 21 день.
Collapse )
Так-то!

upd1/
В редакцию поступила телеграмма о том, что неплохо бы рассказать про LSP — принцип подстановки им. Барбары Лисков. Редакция продолжает отвечать за базар, прямо в этом посте.
Collapse )

(no subject)

Господин Т-в, известный бывший кащенази, оказывается, серьёзно занялся функциональщиной в финансовых областях. Само по себе -- замечательно, я считаю.
А вот что мы читаем про зависимые типы: http://sorhed.livejournal.com/538077.html . Сначала я тоже было достал свой инструмент и даже как бы приготовился его любовно полировать, жалея, что не могу использовать для практических применений agda/coq (а то и что-то ещё, с зависимыми типами), но что-то меня остановило.
Напомню, изначально проблема в том, что с параметрическим типом, имеющим разные типовые параметры, надо уметь работать различными функциями, зависящими от параметров (как минимум, по критерию "можно/нельзя"), и уметь это статически типизировать.
И тут я начал вспоминать, где же мне приходилось такое делать.
"Ба!", -- думаю я. -- "Да это же обычный Паттерн "Фантомные Типы"! Ну да, универсальная типизация хиндли-милнера плюс параметрическая типизация.
type currency;
type commodity;
type instrument 'asset1 'asset2 = ...;
value some_generic_function : instrument 'a 'b -> some_result;
value function_for_currency1 : instrument currency 'b -> some_other_result;
value function_for_barter : instrument commodity commodity -> some_very_other_result;

И, конечно, небольшая ловкость рук в реализации значений с типом instrument 'asset1 'asset2. Однако, в целом, там всё можно свести к паттерн-матчингу (и assert false, например, для случаев, которые типизация явно не пропустит), а то и к более продуманным типам, допускающим подтипизацию (полиморфные варианты и объекты).
После изготовления -- оформить в модуль (надеюсь, в х-е они есть? ну, такие, с сигнатурками.) и использовать строго-типизированный интерфейс. При желании -- оформить как private type и открыть read-only доступ к представлению значений с типом instrument 'asset1 'asset2.

Хотел ещё Вставить картинку Вставить медиаролик Отключить автоформатирование, но уже запечатал конверт. Всем чмоке!

upd/
Ах да, вот ещё что имел ввиду автор: окамловское решение -- фууууу, потому что оно тупое, работает, даёт нужную типизацию и всё такое, а зависимые типы -- ваааау, потому что cs-ёбство для посвящённых, не реализованное почти нигде в практических языках программирования.