ATS: первые впечатления

[thedeemon]

Занялся я тут изучением ATS и в качестве учебного примера взял задачку nponeccop'a про фильтрацию IP адресов. Дабы не изобретать колеса, взял простое и красивое решение antilamer'a и попытался его почти дословно перевести.

Получилось 108 строк на ATS. Собранное версией ATS 0.2.5 под Cygwin'ом оно работает у меня в полтора раза быстрее, чем антиламерское решение, собранное GHC 6.12.1 (с ключом -О2). На тысяче интервалов и миллионе адресов работает 0.8 секунды (версия на хаскеле - 1.2 с), на 10 миллионах адресов - 8 секунд (а решение на хаскеле 12 с). Ради корректности сравнения оба варианта выдают один и тот же результат (вообще говоря, ошибочный - IP адрес, совпадающий с концом интервала, выкидывается, а интервал из одного адреса и вовсе игнорируется).

Выходит эдакая адская смесь ML, сишечки и теоремодоказательства. Писать на ней тяжело, в первую очередь из-за крайне скудной документации, во вторую очередь из-за довольно странной стандартной библиотеки (представляющую из себя обвешанную зависимыми типами libc и кое-что из базовых библиотек SML), в третью очередь из-за сообщений компилятора, которые выглядят так:

/home/user/ats/bin/atsopt --output ips_dats.c --dynamic ips.dats
/home/user/ips.dats: 3287(line=89, offs=9) -- 3293(line=89, offs=15): error(3):
mismatch of static terms (tyleq):
The needed term is: S2Eapp(S2Ecst(at_viewt0ype_addr_view); S2Eapp(S2Ecst(bytes);
 S2EVar(1284)), S2EVar(1285))
The actual term is: S2Eapp(S2Ecst(at_viewt0ype_addr_view); S2Eapp(S2Ecst(b0ytes)
; S2EVar(1267)), S2Evar(l$3484$3485(6817)))
/home/user/ips.dats: 3287(line=89, offs=9) -- 3293(line=89, offs=15): error(3):
mismatch of static terms (tyleq):
The needed term is: S2Etyarr(S2Ecst(byte); S2EVar(1284))
The actual term is: S2Etyarr(S2Etop(0; S2Ecst(byte_t0ype)); S2EVar(1267))
/home/user/ips.dats: 3287(line=89, offs=9) -- 3293(line=89, offs=15): error(3):
mismatch of static terms (tyleq):
The needed term is: S2Ecst(byte_t0ype)
The actual term is: S2Etop(0; S2Ecst(byte_t0ype))
exit(ATS): uncaught exception: _2fhome_2ffac2_2fhwxi_2fresearch_2fATS_2fIMPLEMEN
T_2fGeizella_2fAnairiats_2fsvn_2fats_2dlang_2fsrc_2fats_error_2esats__FatalError
Exception(1233)
exit(ATS): [ccomp_file_to_file(ips.dats, ips_dats.c)] failed.

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

На первый вариант у меня ушло два дня, но он работал на порядок медленнее хаскелевского. Дело было в том, что удобная для использования функция input_line основана на fgetc и сильно тормозит. А чтобы заменить ее на более быструю fgets ушло еще несколько часов, т.к. там типы сильно сложнее, и то не обошлось без читерства (приведение указателя).

Впечатлений масса, чуть позже распишу подробнее и объясню, что все эти закорючки в исходнике означают. Пока лишь замечу, что мой план начать писать на ATS в стиле ML, а потом постепенно вводить зависимые типы провалился: без зависимых типов и доказательств работать со строками, массивами или вводом-выводом нельзя.

Comments

[diam-2003.livejournal.com]

На FME основан алгоритм доказательства теорем в арифметике Пресбургера (грубо говоря, можно складывать и умножать на константу).

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

[thedeemon.livejournal.com]

С условиями оно как-то справляется. А вот умножения переменных друг на друга (нелинейности) уже само не решает, нужно выписывать доказательства. Пример из учебника: то, что соединение двух списков длиной m и n имеет длину m+n проверяется автоматически, а что соединение m списков по n элементов каждый имеет длину m*n пользователь должен доказать конструктивно, выразив этот факт термом-доказательством, построенным из базовых фактов об умножении.

[diam-2003.livejournal.com]

С условиями, и вообще с "потоком управления" в разных его формах, справляются понятно как: консервативно сливают + навешивают эвристические ограничения, типа учета условий, записанных "понятным способом".

Например, если попросить ATS пофильтровать список, про результат можно сказать только то, что он имеет длину не больше исходного списка (консервативная оценка сверху). Аналогично для "взять первые k элементов списка".

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