*академота

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 >

gds 08.09.2012 14:34

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

gds 05.09.2012 18:47

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

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 →

gds 15.02.2012 13:47

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

Do you really want to delete ?

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

gds

gds