Список курсовых/миникурсовых

Темы и задачи про функциональное программирование, С++ & Qt и low-level programming .

В задачах более менее понятно как и что делать, можно оценивать трудоемкость и количество времени/труда, которые нужно положить на доделывание. В темах дается общая картина, должны быть видны первые шаги, но оценивать трудоемкость и количество времени на выполнение затруднительно. Из тем надо выбирать подзадачи на "курсовые".

На сколько я понял, курсовой в 4м семестре нет, есть что-то типа неё, неофициальное, с примерно теми же требованиями, но короткими сроками.

11.02.2018 Добавлена задача про объекты в Qt и тема про SIMD.

Задачи

Парсер для ReasonML/OCaml с восстановлением от ошибок

Так как погромисты на Java не могут никак осилить синтаксис нормальных функциональных языков программирования, в Bloomberg (а потом и Facebook) было предложено совершить ход конём и немного исправить испортить синтаксис уже имеющегося языка функционального программирования OCaml, чтобы он был более похож на привычный синтаксис с фигурными скобками и точками с запятой. Получившийся в результате ReasonML, хомячкам вроде понравился.

С таким подходом вроде бы всё хорошо, но есть проблема для чистокровных OCaml программистов: язык действительно сильно похож, но непохожести очень сильно бесят, никак не получается выкинуть из головы выученный синтаксис и пользоваться новым, потому что то, что видно на экране очень сильно напоминает "старый" синтаксис OCaml. В итоге получаются ошибки, которые очень глупые, но компилятор ReasonML всёравно не доволен. Например:

Вот пример кода на OCaml:

type 'a expr = Const : int     -> 'a expr
             | App   : 'a * 'a -> 'a expr
             | Lam   : string * 'a -> 'a expr

let foo e = match e with
  | Const n -> n
  | App (l,r) ->
      let () = print_endline "blabla" in
      r
  | Lam (s, b) -> b

А вот, что получается при трансляции в ReasonML.

type expr('a) =
  | Const(int): expr('a)
  | App('a, 'a): expr('a)
  | Lam(string, 'a): expr('a);

let foo = e =>
  switch (e) {
  | Const(n) => n
  | App(l, r) =>
    let () = print_endline("blabla");
    r;
  | Lam(s, b) => b
  };

Парсер ReasonML на основе Menhir по ссылке.

Хочется в некоторых местах расширить парсер ReasonML, чтобы он мог разбирать также в том случае, если куски кода были написаны на OCaml (должно случаться, когда программист не успел ещё перестроиться на новый синтаксис). Таким образом парсер будет в некотором смысле восстанавливаться от некоторых ошибок, и в перспективе сообщать программисту "нажмите Alt+Enter+Enter, чтобы исправить Ваш OCaml на соответствующий ReasonML".

Предлагается расширить парсер(грамматику) ReasonML дуальными правилами для OCaml конструкций и генерировать синтаксическое дерево, где куски AST будут отмечены либо как ReasonML, либо как OCaml. Аналогично, можно расширять парсер OCaml синтаксом Reason. Планируется, что работа будет в основном про дополнение новых правил синтаксического анализа, без полного переписывания сузществующих правил.

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

Начинать с:

Краткого обзора синатксиса OCaml и Reason
Краткого обзора мануала по menhir
Добавления дополнительных правил парсинга в тех местах, где синтаксисы разнятся и это легко исправить.

Про создание Qt объектов в контексте OCaml + QML

Моя поделка предоставляет некоторый интерфейс, для создани GUI на Qt/Qml. Наивное использование работает из коробки. Продвинутым использованием является создание своих собственных классов и объектов, чтобы давать к ним доступ со стороны Qt/Qml, а вызываться будут методы написаные не на Javascript (официально это С++ , в моем контексте — OCaml). На данный момент (уже реализовано), пользователь должен

Проаннотировать класс на OCaml.
Система сборки, увидит, что внутри есть интересный класс, и сгенерирует соответствующую обертку (.h и .cpp файлы) со стороны С++ .
Meta object compiler (a.k.a. moc), постаяляемый вместе с Qt, сгенерирует по .h файлу нужный .cpp файл.
Всё скомпилируется и слинкуется в исполняемый файл.

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

либо сократить фазу кодогенерации;
либо избавиться от неё совсем.

Чтобы сократить фазу кодогенерации (избавляясь от второй фазы с moc) можно использовать Verdigris. По сути надо по описанию класса на OCaml генерировать другой С++ и подправить линковку. Это задача номер 1.

От кодогенериации можно попробовать избавиться совсем. В Qt каждый класс, у которого присутствует макрос QOBJECT в реализации, обладает метаинформацией, которая позволяет узнать какие методы и свойства у данного класса есть. Таким образом можно попробовать динамически изменять эту таблицу (добавлять и удалять методы и свойства), тем самым позволяя создавать объекты C++ не проделывая никаких кодогенераций в явном виде. С этих подходом скорее всего будет некоторое количество граблей и подводных камней, первым из них следует назвать, что формат метаинформации может быть прибит к конкретной версии Qt и меняться с эволюцией Qt (тем самым мы закрепляемся в работоспособности к конкретной версии Qt). Это задача номер 2.

Здесь есть пример как добавлять динамически свойства, надо его расширить добавлением методов в контексте OCaml. Более того, если мы научимся брать уже соединенный работающий объект и расширять его свойствами и методами, то мы получим то, что в Javascript называется functional mixins.

Задача подразумевает некоторое взаимодействие и с OCaml, и c C/C++ . Взаимодействие с C сейчас сделано наивно, но можно попробовать воспользоваться чем-то более высокоуровневым от создателя биндингов OCaml к QtWidgets.

Задачи про miniKanren

У нас в лаборатории есть некоторая "тусовка" на тему реляционного (логического) программирования на miniKanren. Если кратко, то это DSL, чтобы относительно естественно решать переборные задачи, например, "перебери мне все программы, и дай те, которые возвращают свой текст". Есть ещё своя реализация miniKanren, которая называется OCanren, на функциональном языке программирования OCaml (он более дружелюбен к новичку, чем Haskell, ИМХО, конечно же).

Скажу сразу, miniKanren — это околонаучная штука на любителя.

Concurrency/parallelism для miniKanren

Полный перебор жутко тормозит по определению, а его мы пока запускаем только на одном ядре. Хотелось бы поставить эксперимент с использованием concurrency, которая есть в "изкоробочном" компиляторе OCaml. А затем, если всё продолжит работать правильно, то воспользоваться неофициальной версией компилятора multicore OCaml (она в разработке). Они там сделали что-то прикольное с использованием algebraic effects и утверждают, что API многопоточности гораздо адекватнее, чем в Java. Я не проверял и поверил товарищам из английского Cambridge на слово.

Заранее отвечаю на вопрос с попыткой развести срач. Python.

Про мемоизацию

Женя делал tabling (мемоизацию для логического программирования) для OCanren некоторым способом, но есть ещё и другой. Разумеется, всё придумали до нас, и нужно только прочитать и реализовать. Нужно прочитать Substitution Tree Indexing by Peter Graph. У меня была PDFка, если надо будет — перешлю.

Error messages

Когда мы адаптировали miniKanren c нетипизированного Scheme на строго статически типизированный OCaml у нас получились довольно длинные типы, которые неудобно читать в тексте сообщений об ошибках компиляции. Хочется сделать плагин к компиялтору, который будет преобразовывать сообщения об ошибках в более специфичный для miniKanren вид. В самом компиляторе уже есть плагины (мануал), которые позволяют добавлять хуки кое-куда, но не туда куда нам надо. Нужно докрутить хуки, чтобы можно было видоизменять сообщения об ошибках на более читаемые для предметной области.

Про доделываение механизма quotation/antiquotation

У нас есть проект GT, про генерацию кода (код представляется как AST) по объявлениям типов. В нём поддерживается работа с AST OCaml (a.k.a. PPX), а также с несколько устаревшей AST Camlp5. И для той и другой штуки существуют механизмы quotation/antiquotation, но каждая реализация работает со своим видом синтаксического дерева и не совместима с другим видом синтаксического дерева. Поэтому в GT мы вынуждены генерировать синтаксические деервья (т.е. код) без quotations, а с использованием банальных вызовов функций конструирования, что очень неудобно.

Предлагается посмотреть на то, как сделан механизм quotation для PPX, почитать README и сделать клон, который

генерирует не какое-то AST, а вызовы функций, которые генерируют AST. Так мы сможем подменять реализации и получать генерацию разного вида AST
понять как устроен metaquot и может быть поддержать неподдержанные синтаксические конструкции: например сейчас никак нельзя использовать quoataiton для классов и объектов

Темы

Про верификацию функциональных программ с SMT солверами

Очень непрактичная тема, потому что в функциональных программах багов нет. :)

И да, это не верификация в стиле Coq.

Когда пытаются сделать верификатор языка, первым вопросом встает дилемма: будем мы делать верификатор какого-то ограниченного искусственного языка программировния с минимальным набором фич, или мы возьмем какой-нибудь существующий практичный язык программирования и сделаем верификацию для него?

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

Их нужно добавить очень много, чтобы получилось что-то соответсвующее реальному языку.
Нужно планировать новые фичи, чтобы не приходилось всё переписывать. В некотором смысле список фич, которыми будем расширять, должен быть известен заранее.
Добавление одной "неправильной" фичи, может сделать задачу верификации неразрешимой. Другими словами приблизиться к концу и доделать может не хватить сил по объективным и субъективным причинам. Подход к верификации может оказаться полностью несостоятельным в самом конце, когда появится фича, которую невозможно поддержать при данном подходе

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

Очень часто надо будет поддержать все фичи языка до конца, потому что даже стандартная библиотека использует все фичи (потому что может). Т.е. нет никакой промежуточной точки, что сказать, что мы решили задачу частично
Практические языки очень богаты, поэтому это просто уйма работы. К тому же арифметика указателей это жуткая боль для верифицирования, много где она есть, но лучше бы её не было.
Практические языки дизайнились как попало, так что поприветсвуйте кучу странных граблей, когда в С# у значения null нет типа от слова совсем.

На 4м этаже бойцы занимаются верификаций с SMT солверами языка C# и имеют там некоторые неразрешимые проблемы. Хочется сделать верификацию языка, который адекватно задизайнен (в отличие от C#), а именно Haskell или OCaml. Ожидается, что это должно быть лучше C# потому что

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

Замечание: OCaml можно заменить на Haskell. Просто первый и компилятор его я знаю лучше и больше смогу помочь.

Замечание: Задача чрезвычайно сложная интересная.

Milestone номер какой-то (к чему пока надо стремиться). Чтобы программа

add x y = x+y
iter f s n | n<0 = s
iter f s n       = f n (iter f s (n-1))

превращалась в формулы (в синтаксисе SMT2lib)

(rule (=> (= z (+ x y))
          (add x y z )
))

(rule (=> (and (<= n 0)
               (= m s))
          (iter f s n m)
))

(rule (=> (and (> n 0)
               (iter f s (- n 1) p )
               (f n p m))
          (iter f s n m))

Всё можно делать в лоб, но если очень хочется, то можно и что-то почитать: раз и два.

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, почитать формальный текст можно тут и тут.

Про GUI и функциональное программирование

Вообще, проектирование GUI можно делать двумя разными способами: можно делать GUI на том же языке, что и бизнес-логику, а можно разносить в несколько языков. Преимуществом первого подхода является то, что разработка ведется на одном и том же языке (не надо учить ничего нового лишнего). Недостатком первого и преимуществом второго подходов является то, что у нас появляется некоторый DSL для проектирования GUI. Этот DSL удобнее чем просто писать код: создавать объекты-кнопочки и складывать их в контейнеры (кто делал GUI на Java+Swing, тот меня поймет).

В мире GUI интерфейсы фреймворки эволюционировали большую часть времени только в рамках объектно-ориентированной парадигмы (хотя в последнее время в моду вошла реактивность). Поэтому, большинство крутых GUI фреймворков делалось для С++ и подобных языков. Функциональным языкам оставалось налаживать взаимодействие с писаными на C++ классами, чтобы элементы управления можно было создавать из кода на OCaml/Haskell. В результате получились биндинги к Tck/Tk, GTK+, которые выглядят так же отвратительно как Swing в Java. Создавать GUI фреймворки только для функциональных языков являлось непрактичным.

В нулевых-десятых годах появились способы проектирования GUI, которые не так явно завязаны на использовании ООП, они предлагают в том числе DSL для проектирования GUI и подерживают аппаратно ускоренный рендеринг через OpenGL. Примерами могут быть WPF, JavaFX и Qt/QML. Лично я занимался созданием библиотеки для использования Qt/Qml для OCaml. По сути QML является языком разметки GUI с поддержкой реактивного программирования, и скриптов на Javascript, чтобы делать простые действия в GUI (например менять цвет чего-то там в зависимости от выбранного в ComboBox). Бизнес-логика, от которой требуется надежность и производительность (чатайте, типобезопасность и скорость), по задумке Qtшников должна писться на С++ и легко интегрироваться с Qt/Qml.

Поделку про OCaml и Qt/QML я сделал, но она не была оценена по достоинству у сообщества камлистов, я полагаю потому, что статически типизированные программисты априори с подозрением смотрят на плохотипизированный скрипт внутри Qt/QML.

Также, говоря про GUI, нельзя не упомянуть веб и браузеры. Javascript захватил мир веба по историческому недоразумению; народ плачет, плюется, но продолжает есть кактус, потому что поделки в стиле TypeScript с gradual typing на борту как-то не взлетают. Но программы на Javascript как-то делаются и кое-как работают. Сейчас движки для создания приложений на основе Javascript и движка HTML страниц (читайте, Electron) заползают и на десктоп, поэтому мы радостно наблюдаем как Discord, банальный групповой чатик, зависает с пожиранием гигабайта оперативы.

Пару лет назад появился ещё один способ для типобезопасного программирования для web, а именно, ReasonML, который является

языком OCaml, который прозрачно компилируется в Javascript
языком OCaml с "испорченным" синтаксисом: фигурные скобочки возле каждого объявления функции, как в Javascript; некаррированный синтаксис для вызова функций (с кучей ненужных скобочек и запятых), как в Javascript; объекты с синтаксисом как Javascript; изкоробочной поддержкой библотеки дизайна компонент интерфейсов React (от Facebook). Короче, всё чтобы хомячки из Javascript приняли новый язык. и они походу его действительно принимают.

Теперь стоит сказать про новоиспеченный проект Revery, где народ на ReasonML делает новый (ещё один новый с нуля, Карл!) фреймворк для клепания GUI, с блекджеком, OpenGL и реактивным программированием. Мотивацией служит отказ от Electron для создания шустрого легковесного кроссплатформенного тулкита. Это всё конечно логично, но давайте лучше

возьмем синтаксис ReasonML;
HTML+ReactJs синтаксис будем транслировать в компоненты Qt/Qml;
OCaml/ReasonML логику будем транслировать в Javascript (ReasonML уже умеет это делать);
автоматически получить возможность линковаться с большим количество проектов, которые уже сделаны в инфраструктуре Qt;
PROFIT.

Сейчас Revery на уровне синтаксического дерева транслирует синтаксис HTML в отрисовку GUI. Хочется поставить эксперимент, чтобы HTML/ReactJs компоненты транслировались в Qt/Qml, всё линковалось и запускалось.

Первый milestone. Все HTML-like конструкции <view бла-бла> бла-бла</view> должны транслироваться в отрисовку Qt/QML окошка с "Hello world". Функция UI.start должно просто показывать это новое окошко.

Автовекторизация в компиляторе

Тема для инетерсующихся ассемблером

В компиляторе OCaml, на сколько я знаю, с автовекторизацией SIMD дела обстоят никак. Вот тут те инстукции, которые компилятор знает. Предлагается найти какие-нибудь примеры, где SIMD дает прирост производительности. И наладить автовекторизацию.

Вон некоторые реализации JVM умеют это делать при JITтинги, чем мы хуже?

Вот какие-то ссылки

Does a compiler use all x86 instructions?

https://www.agner.org/optimize/optimizing_assembly.pdf

Список инструкций

https://blog.janestreet.com/what-is-gained-and-lost-with-63-bit-integers/

Write an assembly superoptimiser supporting AVX and upcoming Intel processor extensions for the MPIR library and optimise MPIR for modern processors

Про автовекторизацию в LLVM

Про добавление поддержки новых языков в QtCreator IDE

Начиная с версии 4.8, в QtCreator завезли поддержку Lnaguage Server Protocol и это означает, что теперь можно малой кровью полчать плагины для языков, подсоединяя бэкэнды для OCaml, ReasonML или Haskell

Берите функциональный язык, который нравится и делайте.

На вопрос "почему QtCreator?" надо рассказываться про прожорливость IDE на базе Electron (Atom, VsCode), криворукость горячих клавиш в Emacs и быть готовым учавствовать в сраче.