Реализацию АВЛ-дерева (это такой подвид деревьев поиска), к которой я имею непосредственное отношение, включили в поставку ATS.

Чем она отличается от других реализаций, коих много? Перечислим:

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

Я написал небольшую заметку по использованию.

Хотелось бы еще сказать следующее. Конечно, работа представляет хороший пример программирования, совмещенного с доказательством теорем, но это не так важно! Важно другое, а именно то, что этим можно действительно пользоваться.

Можно посмотреть с другой стороны: известно, что самобалансирующиеся деревья поиска (такие, как дерево АВЛ) очень трудно запрограммировать, потому что сравнительно несложные инварианты, требуемые для корректности, трудно соотносятся с кодом. Но в нашем случае проблема значительно упростилась благодаря использованию системы типов.

Прошедшие три месяца я занимался разработкой в области веб-ГИС (web-based GIS). Точнее, ситуация была такова:

• у нашего заказчика есть карты и справочники
• заказчик хочет, чтобы у его клиентов появилась возможность просматривать эти карты посредством обычного веб-браузера

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

По совету Werser'а решил посмотреть другие рамы (для велосипеда). Нашел Surly Cross-Check (кроссовые рамы это, оказывается, редкость), даже подумал, что можно заказать.

Тут проблема: если заказывать с Тайваня, то за пересылку возьмут 600USD! Сама рама при этом стоит 380USD. Вот такие дела.

Об этом велосипеде я уже писал в своем блоге, а теперь прошу посмотреть фотографии.

Вот есть такая штука, которая называется "сопрограммы" (coroutines).

Вопросы таковы:

• где используются сопрограммы (тут нужны естественно, иллюстративные примеры, достаточно большие, чтобы быть реалистичными, и достаточно маленькие, чтобы их можно было разобрать по кирпичикам, не прикладывая очень больших усилий)
• для чего они полезны (и для чего бесполезны)
• как они реализуются на современных компьютерах
• каковы их теоретические основания (например, какое отношение они имеют к продолжениям, в т.ч. к ограниченным)

Самое глухое для меня в данный момент -- это первый вопрос. :) Так что, если кто-нибудь знает ответы -- милости прошу.

В марте месяце один веломастер собрал мне велосипед на основе ХВЗ Старт-Шоссе (спецзаказ, рама начала 80-х). В общем-то, кроме рамы с вилкой, ничего от ХВЗ не осталось.

Извините, фоток не будет. Это моя очередная скучная запись. :)

Так сказать background:

• OpenGL ES 2.0 является стандартным API для работы с 2D и 3D аппаратно-ускоренной графикой на встраиваемых системах
• ATS это язык программирования, совмещающий программирование с доказательством теорем, и позволяющий программисту использовать зависимые и линейные типы в практическом программировании

Написал binding к OpenGL ES 2.0 на ATS, а также несколько тестовых программ, смотреть на Google Code.

Среди тестовых программ интерес более-менее представляет одна -- загрузка Wavefront OBJ. Вкратце, реализован лексический и синтаксический разбор, как принято в компиляторах. Посмотрим, каковы будут последствия такого решения.

Написал простой, но в чем-то довольно сложный рейтрейсер.

Что именно оно делает? Оно рисует сцену (на данный момент сцена представлена множеством сфер ;)) методом трассировки лучей, и выводит результат визуализации в файл формата TGA.

Отличительными качествами являются:

• использование продвинутых фишек системы типов ATS для достижения практической цели (мы используем линейные и зависимые типы для обеспечения уверенности в том, что у программы есть некоторые желаемые качества)
• как заметил кое-кто в списке рассылки, это первая нетривиальная программа на ATS, написанная человеком вне кафедры CS Бостонского универа
• уже сейчас рейтрейсер (точнее, рейкастер) довольно быстр, если его сравнивать с аналогами на других ФЯП (Haskell и OCaml) -- хотя о производтельности говорить рано, нужно разработать методологию оценки этого дела, которой можно доверять
• в нем используется парадигма "программирование с доказательством" для того, чтобы иметь возможность использовать некоторые фичи, которые в других языках считаются небезопасными или ведущими к сложноотлавливаемым ошибкам (такие, как арифметика указателей, явное выделение памяти, преобразование указателей) -- и исключенные из этих языков

Надо заметить, что высокая *точность* системы типов сыграла большую, положительную роль в разработке. Теперь вопрос, конечно же, в том, как сделать этот рейтрейсер таким же быстрым, как и его альтернативы на C/C++, не потеряв гарантий полезных свойств.

Остальная инфа тут: mathdev.org/node/24 (включая картиночки).

Почитываю время от времени журнал (кстати, недавно вышел новый номер).

Сегодня увидел комментарии на linux.org.ru и немного удивился: кому-то обязательно нужно смешать авторов с грязью. Теряюсь в догадках, зачем.

Сам по себе журнал хороший (рекомендую интересующимся), но я бы его переименовал, поскольку значение слова "практика" у людей с повышенной прагматичностью сильно отличается от того, что в него вкладывают другие (например, для некоторых "практика" это "копипаст решений с веба, а затем их допиливание до нужного вида", "работа на результат" -- как если бы "работа на процесс" не давала результатов ;)). Наверное, это и создает эффект отторжения.

Почитал немного статьи о линейной логике. Это такая логика, которая оперирует ресурсами (нечто, что можно произвести и истратить), а не вечными истинами.