Алехандро Серрано из 47 Degrees рассказывает, почему зависимые типы круто:
https://www.youtube.com/watch?v=JboZel47XU0
В пару к этому докладу хорошо идет доклад Виталия Брагилевского с f(by) о том, почему зависимые типы не круто:
https://www.youtube.com/watch?v=ohG-PRwOorA
¯\_(ツ)_/¯

Если вас задолбало, что вам присылают аудиосообщения там, где можно было обойтись текстом, есть замечательный вариант ответа:
https://vsychov.github.io/gif-generator

Верификация корректности музыки с помощью системы типов:
https://www.infoq.com/articles/type-systems-verifying-musical-correctness

TL;DR: музыкальные композиции могут быть проверены с помощью системы типов, чтобы сделать негармоничные переходы между нотами непредставимыми. Для этого используется библиотека для хаскеля Mezzo и приводятся примеры с завтипами на идрисе. «Корректность» музыки вообще расплывчатый термин, поэтому в статье применяется дескриптивный подход — «если музыкальная тема отклоняется от ожидаемой модели, то это необычно» — и построение матрицы энтропии для различных комбинаций переходов от ноты к ноте.

Опубликовал перевод статьи об истоках математической нотации из журнала Математической ассоциации Америки:
https://habr.com/ru/post/490520
Это четвертая статья из цикла, но именно она показалась мне наиболее интересной.

Смотрите, какой смешной мудачок:
https://twitter.com/fillpackart/status/1233629821286133761

https://scalacenter.github.io/scala-developer-survey-2019 — результаты опроса от Scala Center за 2019 год подъехали.
Интересно, что Metals показал достаточно высокий процент использования! Это только укрепляет мою точку зрения, что за LSP будущее.

https://www.reddit.com/r/typescript/comments/fda3pw/a_typelevel_lisp_interpreter_ish — интерпретатор лиспоподобного языка на типах TypeScript 🦾
Увы, из-за «Type instantiation is excessively deep and possibly infinite» максимум, что может — посчитать 4×4, а вот 5×5 уже нет.

Немного личного.
В общем, что-то во мне надломилось и я решил уйти из TypeScript-коммьюнити. Старые библиотеки (если кому-то они нужны, лол) вроде fetcher-ts или circuit-breaker-monad буду поддерживать на уровне совместимости с мажорной версией fp-ts, но нового писать ничего не хочу — надоело бороться с ветряными мельницами. Ебитесь и дальше с «ехал any через any», но уже без меня ¯\_(ツ)_/¯
В течении ~полугода постараюсь конвертировать свой опыт (архитектура + фуллстэк-разработка + ПМ + девопс) под экосистему хаскеля. В идеале — найду проектного ментора и запилю несколько pet-проектов для портфолио.
Хотел написать, как всегда, «не переключайтесь», но именно сейчас то время, чтобы переключить канал. Этот тайпскриптер сломался, несите другого.

Любопытный пейпер: «Asynchronous effects»
https://arxiv.org/pdf/2003.02110.pdf
TL;DR: авторы представляют небольшое лямбда-исчисление λæ для описания асинхронных алгебраических эффектов, язык на его основе AEff, и его формализацию на Агде. Выдержка из аннотации:
«At the heart of our approach is the decoupling of the execution of operation calls into signalling that the operation’s implementation needs to be executed and interrupting the computation with the operation’s result, to which the computation can react through a previously installed interrupt handler.»

Проснувшись однажды утром после беспокойного сна, Грегор Замза обнаружил, что он у себя в постели превратился в девопса.

#музыкальная_пауза
Жыве Беларусь! 🇧🇾
https://www.youtube.com/watch?v=BsL6KP3JSzQ

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

Небольшая открытка @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.