Видео с f(by) 2020 https://www.youtube.com/playlist?list=PLpVeA1tdgfCBwyzQBKz52ZDnrZTHeuTLc&feature=share

Куклев:
Кто живёт в разноязычных средах, тому наверняка знакома проблема, когда хочешь поделиться стихами, песней, да хотя бы шуткой на каком-то языке, которым собеседник не владеет, а в переводе уже не то. Да и не только в языке дело, культурный контекст нужен.

Вот если хочешь поделиться восторгами по поводу музыки, видом с горной вершины, невероятного здания, картины, скульптуры — можно показать близким и друзьям, и хоть в какой-то степени, но всё-таки оценят! А не оценят, так хоть заинтересуются...

Но есть такая очень важная для меня сторона жизни, где я своими восторгами я обычно не могу поделиться ни с кем из близких. Там происходят революции, там прямо при нас, прямо сегодня открывают новые континенты, а показать не могу, не могу поделиться.

Симон Анри в прошлом году придумал слабые модельные категории — это настолько круто, что учебники (конечно, не школьные) переписывать можно, он вообще на верном пути в ближайшее время доказать гипотезу Симпсона и вскультивировать целиком ландшафт этой науки. Эмили Риль — придумала принципиально новый подход к проблеме когерентности, красиво как симфония. Две недели назад Пит показал мне с коллегами Эвдоксовы вещественные числа — способ определить вещественные числа через квазиэндоморфизмы на абелевой группе целых. Харальд Хельфготт (тот самый мужик, который недавно слабую гипотезу Гольдбаха доказал, профессорствующий, кстати, у нас в Гёттингене) — оптимизировал решето Эратосфена просто невероятно круто. Это просто четыре рандомных вещи, но оно там такое всё, искрится как фейерверк и всё время что-то новое. Это так красиво, что дух захватывает, это окрыляет, этим хочется делиться, это хочется показывать. Но тот язык, на котором написана эта поэзия, к сожалению, не знает почти никто, и культурный контекст за вечер не перескажешь.

Кто-то в комментах:
Бы бы признателен за ссылки. Полагаю, не только я.

Куклев:
Оно всё гуглится элементарно:
Симон Анри и новое по части модельных категорий:
https://arxiv.org/abs/1603.02456
https://arxiv.org/abs/1807.02650
https://arxiv.org/abs/1905.05625
https://arxiv.org/abs/1907.05394

Эмили Риль:
https://arxiv.org/abs/1801.07404
и вообще https://arxiv.org/search/?query=emily+riehl&searchtype=all&abstracts=show&order=-announced_date_first&size=50

Эвдоксовы вещественные числа:
https://arxiv.org/abs/math/0405454
и все ссылки из https://ncatlab.org/nlab/show/Eudoxus+real+number

Харальд Хельфготт:
https://arxiv.org/abs/1712.09130
и вообще https://arxiv.org/search/?searchtype=author&query=Helfgott%2C+H+A

https://akuklev.livejournal.com/1299860.html

Тред на реддите, достойный целого поста: https://www.reddit.com/r/haskell/comments/f7zxjb/what_are_the_hardestmost_interesting_perhaps/fijek6f/
Обзор менее часто употребимых схем рекурсии (вроде динаморфизма или дендроморфизма) с множеством ссылок на слайды, статьи, пейперы и видео. Если не знаете, чем себя занять на этих затянувшихся выходных — отличный вариант.

ААААААААААААААААА https://twitter.com/private_face/status/1231512192081649665

Гендер на сегодня: тимлич

Math is your insurance policy: https://bartoszmilewski.com/2020/02/24/math-is-your-insurance-policy
Бартош неспешно рассказывает, почему нужно бросать натягивать CSS-шкурки на вордпресс и садиться изучать математику.

Прекрасный проект, вовсю эксплуатирующий (псевдо)полноту по Тьюрингу системы типов TypeScript. Есть даже решение задачи о N ферзях! Правда, натуральные числа кодируются вручную через словарь, так что данный проект умеет считать только до 10. Кодировка чисел Пеано может с этим помочь, но тогда автор упрётся в ограничение глубины рекурсии при выводе типов.
В любом случае, код хорошо документирован и достоен изучения:
https://github.com/ronami/meta-typing

Статья о функциональной архитектуре от Скотта Влашина:
https://increment.com/software-architecture/primer-on-functional-architecture

TL;DR: принципы функционального программирования — использование функций как основных строительных блоков, композиция, чистота — могут быть применены не только для решения тактических задач в прикладном коде, но и для построения более общей, стратегической картины решения целиком. Скотт Влашин в деталях описывает свой подход — построение крупномасштабных «функций»-воркфлоу, применение слоистой архитектуры (onion architecture), определение ограничений (boundaries) и использование событий как входных и выходных точек решения. В конце затрагивается тема функционального фронтэнда на примере Elm и рекламируется книга автора «Domain Modeling Made Functional».

Алехандро Серрано из 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 будущее.