Волны твиттера принесли прекрасное: 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

Майкрософт выложила в публичный доступ официальный проект Windows Runtime для Rust. Не совсем понятно, почему они просто не забрали под своё крыло проект winrt-rust, но тот факт, что теперь есть официально поддерживаемый крейт, внушает еще больше оптимизма касательно будущего языка.

Доказал на идрисе, что a ++ b = a ++ c -> b = c и a ++ c = b ++ c -> a = b:
https://gist.github.com/YBogomolov/430e55c2ce85be963e85b66954a1d483

Ушло часов 6, наверное, с непривычки. Самое сложное, что было — доказательство appendInjectiveLeft. Пришлось даже нырнуть в Elaborator Reflection, чтобы разобраться, как переписываются доказательства. Официальные доки достаточно лаконичны (чтобы не сказать «скудны»), так что сяду читать пейпер Эдвина Брейди об устройстве компилятора идриса.

— Я не верю в PureScript!
— И что же это, по-твоему, заговор типотеоретиков?

https://twitter.com/p_morphism/status/1257399787973902337

❗️В понедельник, 11 мая, в 11:00 по Москве я проведу воркшоп на тему «Building eDSLs in functional TypeScript». Рассмотрим два подхода — Free монады и Tagless Final. Воркшоп будет проводиться на русском языке.
Трансляция будет здесь: https://www.youtube.com/watch?v=TckVngRxu6M, а не на моем канале, так что советую подписаться на Raini.
Если вы хотите участвовать не просто как зритель, а быть участником голосового созвона — заполните, пожалуйста, форму: https://forms.gle/Yvm5Kcac3JbHUc596.
Для участия в воркшопе необходимо склонировать к себе репозиторий https://github.com/YBogomolov/workshop-edsl-in-typescript. Будет нелишним почитать ссылки, которые указаны в README.

Оказалось, что создали запланированную трансляцию не того типа. Приношу свои извинения.
Вот новая ссылка на трансляцию — на этот раз всё правильно: https://www.youtube.com/watch?v=8VFhePZZGdc

Эмили Рил выложила видео своей лекции «∞-category theory for undergraduates»: http://www.math.jhu.edu/~eriehl/berkeley-logic.mp4
Заметки к лекции: http://math.jhu.edu/~eriehl/berkeley-logic.pdf

В мире есть люди, неиронично назвавшие свой проект pi-hole.
ШТОШ