Functional Programming and Proof Checking Course Details (2012)

Темы в порядке обсуждения на лекциях

В соответствии с планом курса.

Общие замеания

• Все лабораторные сдаются при помощи коммитов в свои репозитории. Желательно до дедлайнов.
• Код от заданий и примеры находятся в репозитории на github.
• В случае каких-то изменений в уже заданных заданиях на этой странице будут делаться пометки в соответствующих местах.
• Репозиторий в котором вами выполняется лабораторная не обязан быть родственником моего репозитория (или использовать git), но пути к файлам должны совпадать.
• Никаких лишних файлов, кроме файлов с решениями заданий и, может быть, README, в главном бранче репозитория быть не должно.
• Дедлайны поставлены для совсем немощных, если явно не указано иного, то ожидается, что работу можно сделать за 0.5-3 часа.
• Подглядывать друг другу в репозитории иногда бывает полезно.

Оцениваемые результаты

Домашняя работа #2

Требуется реализовать небольшую стандартную библиотеку для языка Haskell поддерживающую работу с натуральными, целыми, рациональными числами, списками и деревьями.

Часть первая: примитивы и числа

• Файл: /ITMOPrelude/Primitive.hs (click for задание).
• Если можете, то рекомендую самостоятельно реализовать тестер, проверяющий, что определённые вами объекты ведут себя также как Integer и Rational из стандартной библиотеки. Если не можете, то следует:
  • тестировать руками в ghci
  • и ждать пока тестер напишу я (в ближайшие дни, если не будет лень).
• Добавлять свой (впрочем, как и мой) тестер в основной бранч репозитория не следует.
• Дедлайн: 23:59:59 27 сентября 2012.
• Верхняя оценка по времени: 3 часа.

Часть вторая: списки

• Файл: /ITMOPrelude/List.hs (click for задание).
• Дедлайн: 23:59:59 27 сентября 2012.
• Верхняя оценка по времени: 1 час.

Часть третья: деревья

• Файл: /ITMOPrelude/Tree.hs.
• Сочините определение для неупорядоченного бинарного дерева из элементов некоторго типа с операциями:
  • создание пустого дерева,
  • добавления элемента в вершину дерева,
  • добавление элемента в качестве самого левого, правого,
  • повороты влево и вправо,
  • аналог функции map,
  • аналог функции foldr.
• И положите его в файл по вышеуказанному пути в репозитории.
• Дедлайн: 23:59:59 27 сентября 2012.
• Верхняя оценка по времени: 1 час.

Изменения (более новые внизу)

• Критическое: коммит bbb1381643b7f9406a8ab620b3b75cffb7c3dc92. Переименовывает конструкторы Tri и функции сравнения в более стандартный вид.
• Критическое: коммиты по 1d766d84b2b19a7429eba14efe2605ab6532321a. Добавляют булевы операции и фиксят описания функций в ITMOPrelude.List.
• Мелкий критический багфикс: f0b3c8238327c2512898ecdfacd3e938c1c2afb8.

Домашняя работа #3

Требуется реализовать REPL для нетипизированного $\lambda$-исчисления. Начать следует с «E», «R» и «P» возложить на ghc с его deriving (Show,Read).

• Файл: /UnTyLambda/Interpreter.hs.
• Дедлайн: 23:59:59 12 октября 2012.
• Верхняя оценка по времени: 3 часа.

Домашняя работа #4

Требуется вкрутить в ITMOPrelude всякие интересные тайпклассы. Все “вопросы” и undefined в файлах надо заткнуть.

Часть первая: алгебра

Реализовать классы Monoid и Group, а также их инстансы для типов из ITMOPrelude.Primitive.

• Файл: ITMOPrelude/Algebra.hs.
• Дедлайн: 23:59:59 21 октября 2012.
• Верхняя оценка по времени: 30 минут.

Часть вторая: категории

Реализовать классы Category, Functor и Monad, а также их инстансы для всех типов (для которых это возможно) из ITMOPrelude.

• Файл: ITMOPrelude/Categories.hs.
• Дедлайн: 23:59:59 21 октября 2012.
• Верхняя оценка по времени: 1 час.

Замечание. Да, id и (.) из Category клешится с функциями из модуля ITMOPrelude.Primitive. Это нормально. Решите данную проблему любым удобным способом (не переименовывая функций).

Часть третья: монады через монады

Доказать, что все три определения Monad (стандартное, “рыбка” и fmap/join) эквивалентны.

• Файлы: ITMOPrelude/Categories.
• Дедлайн: 23:59:59 29 октября 2012.
• Верхняя оценка по времени: 30 минут.

Часть четвёртая: сделаем свой State и IO

Требуется реализовать монаду State и мок монады IO через State. IO там смешной, поскольку ITMOPrelude не поддерживает строк.

• Файлы: ITMOPrelude/Categories.hs и ITMOPrelude/IO.hs.
• Дедлайн: 23:59:59 2 ноября 2012.
• Верхняя оценка по времени: 40 минут.

Изменения

• Критические и не очень: до коммита e218d8a7f8aece28d9d510c726b5db23ed55e7e9.

Домашняя работа #5

Написать для термов из UnTyLambda.Interpreter выводилку простых типов при помощи решения системы уравнений.

• Верхняя оценка по времени: 5 часов на выполнение в лоб при условии минимального невладения стандартной библиотекой, 1 час если понять, что делают эти люди (а помочь в этом могут вот эти люди). В целом тема очень интересная, гугление и хождение в ширину по ссылкам очень помогает.
• Выполнение не обязательно. Дедлайна нет, но если успеть сделать к Midterm #1, то мегабонус гарантируется.

Домашняя работа #6

Требуется реализовать простой монадический парсер $LL(\infty)$. Все undefined в файлах надо заткнуть.

• Файлы: Monstupar и Monstupar.hs.
• Дедлайн: 23:59:59 2 ноября 2012.
• Верхняя оценка по времени: 2 часа на выполнение, 2 дня на осознание того, что всё действительно так просто.

Изменения

• Критические и не очень: до коммита e218d8a7f8aece28d9d510c726b5db23ed55e7e9.

Домашняя работа #7

Требуется дописать REPL для нетипизированной лямбды при помощи Monstupar. Все undefined в файлах надо заткнуть.

• Файлы: UnTyLambda/REPL.hs.
• Дедлайн: 23:59:59 4 ноября 2012.
• Верхняя оценка по времени: 3 часа, и ещё день на то, чтобы понять где ошибка (если слушаться комментариев в файле, то день можно сэкономить).

Midterm

Требуется поговорить со мной, что-то написать, получить от 0 до 50 баллов.

Домашняя работа #8

• Изучите как устроены Fusion в bos-text.
• Потырьте (ре-реалируйте) нужные вам части оттуда.
• При помощи ByteArray# из GHC.Base и вашего Fusion реализуйте нижеследующее.
• Выполнение не обязательно. Дедлайна нет, но если успеть сделать к Midterm #2, то мегабонус гарантируется.

Часть первая. Moving average

• Реализуйте moving avegare фильтр.
• Файлы в репозитории: Fusion/Common.hs, Fusion/Average.hs.

Часть вторая. Canny edge detector. Easy parts

• Реализуйте Canny edge detector до “Non-maximum suppression” включительно.
• Входную картинку читайте из PNG и рендерьте в PNG при помощи любой удобной вам библиотеки. Обе картинки можно делать чёрно-белыми.
• Файлы в репозитории: Fusion/PreEdge.hs.

Требования к первым двум частям

• При компиляции с -O2 в результате оптимизаций должена получаться ghc-core программа, работающая в константной памяти.
• Результирующий ассемблерный код должен быть близок к тому, что вы написали бы руками. В ассемблере, генерируемом для первой части нужно полностью разобраться, ну по крайней мере в той части, что считает. Для второй части следует как минимум убедиться, что оно компилируется в циклы и не выделяет ничего лишнего на хипе.
• Вам могут понадобиться unboxed tuples.

Часть третья. Canny edge detector. Hard parts

• Реализуйте оставшуюся часть.
• Эта часть ещё более необязательна (потому что у нас тут не курс вычгеома), но и добиваться оптимального ассемблера тут не нужно.
• Файлы в репозитории: Fusion/Edge.hs.

Домашняя работа #9

Тут какая-то Agda. Условие было выслано в список рассылки.

Экзамен

Требуется поговорить со мной, что-то написать, получить от 0 до 50 баллов.