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

[clayrat.livejournal.com]

а Idris видали? вроде ниша та же - "сишечка с завтипами"

[clayrat.livejournal.com]

http://idris-lang.org/

[thedeemon.livejournal.com]

Больше похоже на недоделанную Агду.
Хаскельный синтаксис, компиляция в Си с "rudimentary FFI" и Boehm GC. На "сишечку с завтипами" как-то не похоже.

[clayrat.livejournal.com]

ну автор заявлял мол IDRIS is intended for research into low-level systems programming

[thedeemon.livejournal.com]

Нет, еще не видел, спасибо за ссылку.

[diam-2003.livejournal.com]

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

Опять же, расово верного Пресбургера далеко не на все разумные применения хватает.

[thedeemon.livejournal.com]

Тут обычно компилятор довольно точно говорит место в исходнике, которое вызвало затруднения. Но в чем именно проблема и как ее решать далеко не всегда очевидно, если ты не китаец из бостонского универа.

В ATS используется Fourier–Motzkin elimination. Не знаю, как он соотносится с Пресбургером, но сложность вроде та же.

[diam-2003.livejournal.com]

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

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

[thedeemon.livejournal.com]

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

[diam-2003.livejournal.com]

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

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

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

[si14.livejournal.com]

>Впечатлений масса, чуть позже распишу подробнее и объясню, что все эти закорючки в исходнике означают
С нетерпением.

[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 как строка передаётся в реальных системах.