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]

извините, понимаю предрассудки, но меня начинает плющить от таких объёмов. 108 строк!
в моём решении символов в 3 раза меньше: http://inv2004.livejournal.com/144767.html

И работает вроде за сходные цифры, если не быстрее (подождём оффициальных результатов).

[inv2004.livejournal.com]

это решение без парсинга, парсинг ещё добавит, но до 108 символов никак не дотяну.

[thedeemon.livejournal.com]

А какая там скорость получается (с чтением адресов и диапазонов из файлов)? Здесь все упирается в ввод-вывод и парсинг адресов, сам поиск-то мало занимает (5% по замерам antilamer'а).

Вообще, все правильно, ATS абсолютно не претендует на лаконичность, наоборот, нужно постараться, чтобы на другом языке написать то же самое длиннее. А все потому, что немалую часть программы составляет доказательство корректности. Там нельзя обратиться к i-му элементу массива или строки, не представив компилятору доказательство, что в массиве/строке есть такой элемент. В этих 108 строках гарантируется, что не будет проездов по памяти, не будет некорректного обращения с файлами и не будет зацикливания в рекурсивных функциях парсинга и двоичного поиска. Кроме того, основной цикл с чтением адресов и фильтрацией работает без выделения памяти и нагрузки на GC.

Ну и нашли с чем сравнивать, К и J - короли троллинга по лаконичности. Только они для марсиан, люди такое читать не могут.

[inv2004.livejournal.com]

Это какие-то несравнимые вещи по-моему. 5% от 2 секунд? это 0.10 секунд на поиск? не очень верится. Я замерял только чистое время, как это требовалось в задаче. А тут 2 секунды, которые зависят от многих факторов, таких как скорость винта и тд + какие-то абстрактные 5%.

Спасибо за наводку по ATL,даже интересно стало. но я выделил из исходного сообщения, что скорость большая.

И про K я уверен, что это не для марсиан, просто почему-то все очень мнительны в плане синтаксиса, например / - это foldl1 , но почему-то foldl1 (+) [1,2,3] всем нравится, а +/1 2 3 - ужасно для инопланетян. Не понимаю.

уровень вхождения в K очень низкий, раз даже я освоил кое-как. весь словарь: 19 слов (*2 так как монада и диада) + 6 adverbs, из них используются в основном только два ' (map) и / - foldl.

[thedeemon.livejournal.com]

Вот тут он чистую скорость на синтетическом тесте упоминает:
http://antilamer.livejournal.com/384832.html?thread=3723584#t3723584
90 млн адресов в секунду.

Я попробую у себя скорость чисто поиска померять, только надо будет разобраться, как в ATS это делается.

Про К: "+/1 2 3" еще вяглядит терпимо, но m:0N,{1+|/x#iph}'1+!#ipl это уже совcем %($*#)/1&*$#/1^%+N*0#;@$;^*.

[inv2004.livejournal.com]

скорость посмотрю - с остальным не согласен. запись ничем не отличается от ~:
только 1+ тут на списках работает, а тут пришлось лишний map вставить.

(:) 0 $ map (\x -> map (1+) $ foldl max $ take x iph) $ map (1+) [0..(length ipl)]

# (manad) = length
!X - [0..(X-1)]
1+ - это как 1+ так и map (1+)
{}'l - это map (\->...) l
x#l - take
/ - foldl1
| - max
|/l - foldl1 max l

мне кажется очень просто, как минимум намного проще чем haskell. Я действительно не понимаю что тут такого сложного, кроме стереотипов, что "как-то странно выглядит".

[thedeemon.livejournal.com]

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

[usovalx.livejournal.com]

О, там ещё и пробелы значащие.

2-2    => 0
2 - 2  => 0 
2 -2   => list(2; -2)

[inv2004.livejournal.com]

Давайте замеряем чистое время на поиск и сравним.

[thedeemon.livejournal.com]

time() из стандартной библиотеки ATS меряет с точностью до секунды, более точного мерила быстро не нашлось, а осваивать FFI и использование QueryPerformanceCounter из под Cygwin'a лень.

Поэтому сделал такой вот цикл с генерацией случайного числа и его поиском:

  fun loop {m:nat} (m : int m, k : int): int = 
    if m = 0 then k else  let
      val ip_lint = mrand48()
      val ip = uint_of_lint ip_lint
      val k1 = if ipgood(ps, n, ip) then k+1 else k
    in
      loop(m-1, k1)
    end

Потом просто позапускал 10 млн итераций и 20 млн итераций и вычел время. Использовался набор из 1000 диапазонов, из случайных адресов чуть больше половины попадают в какой-нибудь из них.
Скорость на Q8200 @ 2.33 GHz: 0.187 cек на миллион адресов.

[inv2004.livejournal.com]

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

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

[thedeemon.livejournal.com]

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

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

[inv2004.livejournal.com]

Я кстати тоже на 0.1с вышел: http://inv2004.livejournal.com/145515.html

[thedeemon.livejournal.com]

Просто чудо какой код, нифига не понятно! :)
Это с парсингом (строка с адресом - число) али без?

Сорри, я тут отвлекся, так у себя поиск и не померял еще.

[inv2004.livejournal.com]

Да, признаться я сам пока к J не привыкну. K очень понятен, J пока приходится в словарь частенько смотреть. Основная проблема тут кстати наоборот - что слова многобуквенные. + не проблема, но не привычно - это составление глаголов с помощию трансформаций: вилок и крючков, зато нет использование параметра по имени.

Это без парсинга. просто число, мне кажется, что мало где ip как строка передаётся в реальных системах.