Курс «Программирование с зависимыми типами на языке Idris»
567 открытий590 показов
Русскоязычный курс от Computer Science Club, посвященный базовым аспектам программирования на языке Idris. Курс записан в 2017 году, лектор — Виталий Брагилевский.
В курсе рассматриваются следующие темы:
- типы как сущности первого класса, функции на типах;
- зависимые типы и зависимое сопоставление с образцом;
- приёмы доказательства равенств, разрешимости и тотальности;
- выражение отношений средствами зависимых типов;
- вычисление эффектов.
Для успешного прохождения курса желательны начальные навыки программирования на языке Haskell или другом функциональном языке программирования.
567 открытий590 показов