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

[inv2004.livejournal.com]

ok, я просто думаю что финальный репорт от nponeccop не скоро будет.

тут кстати mrand48 возможно будет очень медленный?

[thedeemon.livejournal.com]

Если из цикла убрать сам поиск, а оставить mrand48 и остальное, получается 10% от того времени. Т.е. 90% от указанной выше величины таки занимал поиск.

Занятно, сейчас собрал и запустил на ноуте с вистой, там mrand48 все время возвращал нули, если сперва не сделать srand. На рабочем компе с семеркой такого не было, случайные числа генерились и без srand.