*академота

komar 04.02.2013 08:45

Пишу файловое хранилище. Товарищи занегодовали, чего это я какой-то велосипед изобретаю. Я им объясняю, что совать все файлы в одну диру — хуевая идея. Они не верят, говорят про какой-то индекс. Решил доказать и забенчмаркать. Написал строчку на баше и понял, что "| xargs touch" адски тормозит. Взял OCaml:

for i = ... more →

gds 07.01.2013 18:54

"
This reminds me of a funny event at the Haskell workshop 2006. One participant stood up and sincerely proposed that Haskell' standard would find a way to automatically derive a monadic version of a pure expression. Chung-chieh Shan recommended that person to take a look at OCaml...
"
(уже второй раз лезу за этой ... more →

gds 05.11.2012 19:17

Опыт использования Coq на практике, или Как я сам себя отпетушил COQОКОКОКО < http://gds.livejournal.com/65879.html >

komar 18.10.2012 18:11

Правильный программист на haskell:
<voker57> КАТАМОРФИЗМЫ
<voker57> кстати, всегда забываю, что это

komar 17.10.2012 14:37

<voker57> там какая-то хуйня была, в которую можно любой тип завернуть
<voker57> вот передавать значит мап такой хуйни и кастовать во что нужно
<voker57> конечно в компил тайме проверки никакой не будет
<komar> А, ты про то, что хештейблы уебищные?
<voker57> да
<komar> ХУИТА
<voker57> ну, это потому, что мы в ... more →

gds 08.09.2012 14:34

Постил в камлочятик, но запощу и тут.
Есть вероятность, что Олег будет давать интервью. Можно повлиять на вопросы. Присылайте мне, я передам куданадо.
Вопрос про то, не жмёт ли ему череп, я задать хотел бы, но это некультурно. Вопрос про будущее метаокамла уже скинул. Вопрос про субъективное сравнение языков с ... more →

gds 05.09.2012 18:47

"гулял в компании зависимых типов"

komar 01.09.2012 22:08

Посмотрите на этого кукаретника: http://thesz.livejournal.com/1328059.htm...

gds 01.06.2012 12:01

In the Soviet Coq, the monad transformer writes You!

gds 26.03.2012 01:20

сейчас наткнулся на подобную штуку, и немного генерализирую.
при написании веб-сервера на coq обнаружим, что рекурсивная функция, читающая http-заголовки, внезапно потребует доказательства завершимости. По идее, оно должно включить в себя конечность числа символов в прочитанных заголовках, либо конечность как числа ... more →

gds 22.03.2012 09:01

к моему посту #osofnz — Олег Киселёв пишет в caml-list:
"Somehow typed tagless interpreters (embeddings of a typed language) and length-parameterized lists with the append function are the most popular examples of GADTs. Neither of them seem to be particularly good or compelling examples. One can write typed ... more →

gds 12.03.2012 15:56

true <> false
Неожиданно? Однако, это так.
Эта шокирующая истина теперь конструктивно доказана: http://gds.livejournal.com/63887.html

gds 11.03.2012 12:55

http://gds.livejournal.com/63527.html — как обычно, интересуют каменты там либо тут. (не нравится щёлкать на ссылку — не щёлкайте, но копипастить ту простыню сюда я не буду.)

gds 10.03.2012 13:38

coq / ocaml = ocaml / c
крыша едет точно так же, как 10 лет назад от изучения функциональщины.
кстати, по "coq "program framework"" (собственно для написания кода, а не для доказательства) ищется слишком мало всего. Понятно, что фишка новая, но где про неё читать — ума не приложу. Есть идейки?

gds 05.03.2012 14:39

gadt'ы — только для typed [e]dsl evaluation
dependent types — только для проверки границ массивов
дискасс блеять.

gds 05.03.2012 13:20

вопрос про пользу зависимых типов: http://gds.livejournal.com/63409.html — покаментите, если есть мнение. (тут или там — пофиг.)

gds 27.02.2012 10:08

Как-то мне попалась в руки хорошая папира, хоть и от microsoft research, про "eventually consistent transactions": http://research.microsoft.com/pubs/15763...
И довольно удачно, потому что в работе подобное пригодится, вероятно.
И вот, дошли руки прочитать. Отзыв писал другому человеку, но ... more →

gds 21.02.2012 21:42

(кто читал это в чятике, дальше не читайте.)
в качестве отдыха решил изобразить на окамле весьма тупую "топологическую сортировку", бесстыдно эксплуатирующую ленивый порядок вычислений.
исходник: http://paste.in.ua/3901/
почему решил показать — потому что многие люди не уверены, что на окамле подобное возможно ... more →

komar 20.02.2012 21:39

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

gds 15.02.2012 13:47

вот какая хуйня получается, когда композиция функций является навязчивой идеей и сталкивается с неокрепшей психикой: http://evincarofautumn.blogspot.com/2012...

komarElemir 12.11.2011 18:02

> O Y fixed point combinator είναι ένα από τα πιο περίεργα και γοητευτικά "αντικείμενα" που έχω συναντήσει σε αυτό που ονομάζουμε "Computer Science". Γενικά ο Y combinator χρησιμοποιείται για να ορίσουμε recursive anonymous functions.
http://www.dotnetzone.gr/cs/blogs/pallad...

komar 02.10.2011 19:39

<komar> > Microsoft Word Starter Edition.
<komar> Угадай, чей блог я читаю?
<voker57> УГАДАЛ

*академота is used by:

gds

gds