Задачи

Прошлогодние

Темы и задачи прошлого года более-менее актуальны (по-хорошему их надо подредактировать и накопипастить сюда, но потом)

Новые задачи и темы придуманы, но пока не вписаны.

Демка инкрементальных вычислений с матрицами

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

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

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

В планах лежит попытка это опубликовать на тематическм воркшопе GRAPHS NDA.

Руководители Семен Григорьев и Дмитрий Косарев

Компиляция программ на OCaml в lua (занята)

На данный момент при embedded разработке программист строго ограничивается возможностями железа (скоростью процессора и объемом памяти) и спецификой требований к софту: очень часто приветствуется бинарные сборки программ, где отсутсвуют код, которые непосредственно не используется в разрабатываемом продукте. Эти требования существенно осложняют использование проверенных временем библиотек, таких как Qt, boost, и даже glibc. Очень часто программисты вынуждены использовать более-менее высокоуровневые языки программирования (Lua или минималистичную реализацию JavaScript) с небольшим рантаймом (десятки килобайт).

Использовать всю мощь функционального программирования не получается в embedded разработке как по объективным причинам (такие имеют большой объем рантайма, для OCaml — 200 КБ), таки по не очень доказанным (функциональное программирование тормозит).

Предлагается научить генерировать по коду на OCaml код на языке Lua взяв за основу одну из двух уже имеющихся работ по генерации Javascript из OCaml.

  • Можно генерирвать Lua непосредственно из исходного кода OCaml по аналогии с проектом Bucklescript. Плюсы: читаемый код на выходе. Минусы: необходимо поддерживать весь язык OCaml.

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

Руководители Кирилл Смирнов и Дмитрий Косарев

Alt-Ergo (гроб)

Допиливать существующий SAT/SMT solver алгоритмами из мира мат. логики, которые там не сделалны.

На вскидку это

  • unsat core для DPLL/CDCL

  • IC3 и прочие апгрейды его

merlin

IDE для функциональных языков не очень хорошо развиты по нескольким причинами:

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

  • так как потредность в IDE не так ощущается, то мало кто уходит дальше минимальных требований к IDE, которыми явщяются: go-to-definition, показать тип под курсором, подсветка ошибок и прочие мелочи.

Следствие: в области разработки IDE для функциональных языков можно много чего сделать.

Сейчас стандартом IDE для языка OCaml является merlin, который сейчас умеет минимальный набор фич.

Хочется его постепенно допилить:

  • signature help

    • по локации понять из typedtree, что курсор стоит на применении функции

    • понять на каком мы аргументе

    • показать сигнатуру функции + доку (если есть)

  • Выдавать предложения переименовать идентификаторы ради исправления ошибок (например, если человек написал Lsit вместо List)

  • различные умные рефакторинги, в частности whole project renaming. Сейчас это кое-как умеет делать RoToR, но он не умеет делать больше ничего. Хочется повторить удачную реализацию RoToR в merlin.

  • и т.д.

В идеале, работа должна заключаться

  • и в допиливании backend на OCaml, который занимается анализами и содержательной частью вообще

  • и в допливании frontend (например, VsCode), который позволяется редактировать код и вызывать рефакторинги непосредственно

Active Patterns в OCaml (занята)

В Haskell они есть (называются Pattern Synonyms), в F# — тоже, а в OCaml непорядок.

Задача изначально появилась в Кембридже. По ссылке есть описание поддержки не их, но сходной фичи; написано в каком порядке что делать, чтобы начать приближаться к Active Pattern’ам. Иными словами задачи разбивается на две связанные

  • With syntax for patterns

  • Pattern Synonyms a.k.a. Active Patterns

Про OCaml можно спрашивать людей на форуме или в Discord.

Формально это сделано в F# и Haskell, почитать формальный текст можно тут и тут.

На форуме OCaml уже началось обсуждение правильного синтаксиса.

Про парсинг графов с помощью грамматик на Haskell (занята)

Есть статья Efficient Parallel and Incremental Parsing of Practical Context-Free Languages от JEAN-PHILIPPE BERNARDY & KOEN CLAESSEN (pdfку могу выслать), где авторы пишут, что смогли распараллелить синтаксический анализ для некоторых "хороших" грамматик и получить прирост скорости. У доступна реализация на Haskell.

Хотелось бы * вначале проверить что всё действительно работает так хорошо, как написано * применить подход для синтаксического анализа графов

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

Руководители Семен Григорьев (может быть и Дмитрий Косарев подключится).