Я: Мам, я хочу типизацию!
Мама: У нас есть типизация дома.
Типизация дома:

Небольшая открытка @ebanatics

https://twitter.com/AntonKulibyakin/status/1242040849892073472

Ко мне продолжают приходить в личку с вопросами о продолжении стримов по ФП. Видимо, нельзя просто так вот уйти из коммьюнити.
Так что оставайтесь дома и приходите сегодня в 20:00 на стрим по функциональному TypeScript. Рассмотрим паттерн тайпкласса и некоторые простые тайпклассы — Eq, Ord, Functor, Monad, Traversable, etc.
https://youtu.be/pPUguhBZ8JY

Бесплатная книга: «Verified Functional Programming in Agda»
https://dl.acm.org/doi/book/10.1145/2841316
Verified Functional Programming in Agda is the first book to provide a systematic exposition of external and internal verification in Agda, suitable for undergraduate students of Computer Science. No familiarity with functional programming or computer-checked proofs is presupposed.

Bartosz Milewsky & Oli Makhasoeva - Recursion schemes, categorically!
https://www.youtube.com/watch?v=FeG41moU8Xk

Волны твиттера принесли прекрасное: https://twitter.com/vamchale/status/1249076951685398530

TL;DR: в Elm была проблема — паттерн-матчинг по негативным числовым литералам приводил к ошибке парсинга. Эван Чаплицкий не только не исправил этот баг (при этом спросив у автора тикета «Instead of fake examples, can you explain how this comes up?») — он еще и добавил в компилятор текст ошибки, который предлагает использовать вместо паттерн-матчинга if-else.

Вторую неделю не могу перестать думать об этой картинке 😬

Нужно ещё приложение от Zewa «А как какать»

Грант Сандерсон — автор прекраснейшего канала 3Blue1Brown, на который я рекомендую подписаться, — о причинах, почему люди вообще занимаются математикой:
https://www.youtube.com/watch?v=s_L-fp8gDzY

Достаточно интересный пейпер от Андрея Мохова, Нила Митчела и Саймона Пейтона Джонса о системах сборки (Make, Bazel, Nix, Shake, etc.).

Build systems à la carte: Theory and practive
Build systems are awesome, terrifying – and unloved. They are used by every developer around the world, but are rarely the object of study. In this paper, we offer a systematic, and executable, frame- work for developing and comparing build systems, viewing them as related points in a landscape rather than as isolated phenomena. By teasing apart existing build systems, we can recombine their components, allowing us to prototype new build systems with desired properties.
https://www.cambridge.org/core/journals/journal-of-functional-programming/article/build-systems-a-la-carte-theory-and-practice/097CE52C750E69BD16B78C318754C7A4
#paper

Собрал небольшую подборку видео о программировании на Idris — языке с зависимыми типами, которому не помешает щепотка популяризации.

https://www.youtube.com/watch?v=X36ye-1x_HQ — доклад, с которого для меня всё началось: Эдвин Брэйди, автор языка, рассказывает, что такое вообще Idris и какие преимущества он может дать программисту.
https://www.youtube.com/watch?v=4i7KrG1Afbk — отличный доклад Брайана МакКенны о практических применениях Idris без единого примера сложения векторов, ура!
https://www.youtube.com/watch?v=DRq2NgeFcO0 — выступление Эдвина Брэйди о нововведениях в разрабатываемом сейчас Idris 2 — в частности, о Quantitative Type Theory, которая позволяет выражать количество «использований» (consumption) аргумента функции.
https://www.youtube.com/watch?v=QMPum88xluE — доклад от Сьюзан Поттер о работе с AWS при помощи Idris. На мой вкус, слишком много времени уделено детальному разбору соответствия Карри-Ховарда, но часть про работу с AWS прекрасна.
https://www.youtube.com/watch?v=AWeT_G04a0A — доклад от Дэвида Кристиансена о представлении паттерна универсумов в Idris на примере программы по работе с изображениями.
https://www.youtube.com/playlist?list=PL-_cKNuVAYAXFRLj6n2nDjI1cyHjuI3HI — ну и куда же без цикла лекций от Виталия Николаевича Брагилевского (@bravit_about), где язык разбирается с самых азов по книге Эдвина Брэйди «Type-Driven Development with Idris».

Снова открытка @ebanatics

О, смотри, тут тебя показывают

Вскрикнул

О, новая версия Mu зарелизилась. Интересно, что интерфейс Mu-Haskell и Mu-Scala разительно отличается, потому что 47 Degrees хотят развивать каждую из библиотек семейства Mu в идиоматичном для языка ключе. Будет любопытно взглянуть, что будет в Mu-Kotlin, которая заявлена как coming soon.
https://www.47deg.com/blog/mu-haskell-0-3