Project

General

Profile

Actions
Эта страница предназначена для свободного редактирования всеми участниками семинара
Замечания и дополнения приветствуются

Цели

  • знакомство незнакомых с основопологающими, но нетривиальными возможностями языков с развитой системой типов (например, параметрический и ad-hoc полиморфизм);
  • знакомство незнакомых с прагматикой функциональных языков, неизвестными приёмами над известными языковыми конструкциями;
  • приобщение специалистов по спецификации, тестированию и верификации к терминологии, приёмам и техникам функционального программирования.

Интересные темы и направления для будущих семинаров

  • объяснение техник, которые используются в наших библиотеках (и не только):
    • рекурсивные схемы;
    • lens/optics/category-arrow-iso-semiiso;
    • Functor Functors / Higher-Kinded Data;
    • property-based testing (на странице Haskell ссылки на много библиотек);
    • ...;
  • расширения haskell (language extensions):
    • все, что связано с проблемами поиска instance и т.д., как он устроен, что за ошибки происходят при использовании MultiParamTypeClasses+FunctionalDependencies:
      • OVERLAPPABLE/OVERLAPPING
      • FlexibleInstances/FlexibleContexts
      • UndecidableInstances
    • TypeFamilies + DataKinds и все-все-все - typelevel данные, аннотации, вычисления и все такое;
    • ExistentialQuantification;
    • ...;
  • библиотеки -- как выбрать, когда несколько; сравнения, скандалы, интриги, расследования;
  • системы эффектов в функциональных языках
    • monad transformers, MTL;
    • freer monads;
    • capability;
    • algebraic effects;
    • ...
  • зависимые типы (в частности, в применении к спецификации);
  • ???.

Семинары (темы и планы)

01.11.2019 -- Тайпклассы Haskell и для чего их можно использовать

Слайды: 2019.11.01-typeclasses-n-polymorphism.pdf

13.11.2019 -- Данные не нужны: Что знал Алонзо Чёрч еще 80 лет назад

Слайды: 2019.11.13-church-encoding.pdf
Слайды той же лекции, прочитанной для другой аудитории: 2020.03.06-chuch-encoding-bis.pdf (изменённое соотношение сторон, мелкие исправления + пример из первой лекции)

20.11.2019 -- Как построить (символьно интерпретируемый) EDSL

Слайды: 2019.11.20-symbolic-edsl.pdf

04.12.2019 -- Как достигать желаемых эффектов

Слайды: 2019.12.04-mtl-and-effects.pdf

18.12.2019 -- Рекурсивные схемы: рекурсия в типах и коде

Слайды: 2019.12.18-recursion-schemes.pdf

22.01.2020 -- Зависимые типы и соответствие Карри-Ховарда. Или интерпретация Брауэра-Гейтинга-Колмогорова. Свежие идеи, которым 90 лет

Слайды: 2020.01.22-bhk-deptyp.pdf
Слайды той же лекции, прочитанной для другой аудитории: 2020.02.19-bhk-deptyp-bis.pdf (чуть расширенное введение + исправления)

05.02.2020 -- Model-based тестирование протоколов и парсинг

Слайды: 2020.02.05-mbt-and-parsing.pdf

Updated by Denis Buzdalov 5 months ago · 17 revisions