Functional Programming and Proof Checking Course Details (2012)

by Jan Malakhovski

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Изменения

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

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

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

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

Изменения

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

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

Midterm

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

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

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

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

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

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

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

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

Экзамен

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