*академота

http://dump.bitcheese.net/files/ecugize/...

#tsezto

3 comments

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

for i = ... more →

#tieggn

11 comments

"
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 →

#tioeof

add comment

Coq quick reference: https://wiki.mq.edu.au/display/plrg/Reso...

#tfifzf

add comment

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

#thfgnh

1 comment

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

#ttnohi

7 comments

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

#ttgeis

3 comments

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

#toehgt

18 comments

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

#tosifn

3 comments

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

#toihng

3 comments

http://dump.bitcheese.net/files/okikyze/...

#onnizg

23 comments

In the Soviet Coq, the monad transformer writes You!

#onotgi

3 comments

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

#osgisi

add comment

к моему посту #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 →

#osehhh

2 comments

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

#osheot

2 comments

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

#oshhoh

add comment

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

#ostnnh

13 comments

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

#osofnz

7 comments

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

#osofez

add comment

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

#oinhtf

2 comments

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

#oiegoe

2 comments

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

#oiefnt

2 comments

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

#oiigzt

add comment

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

#othzzf

add comment

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

#oznnsz

add comment