Forwarded from PONV Daily (Sergey Kucherenko)
Куклев:
Кто живёт в разноязычных средах, тому наверняка знакома проблема, когда хочешь поделиться стихами, песней, да хотя бы шуткой на каком-то языке, которым собеседник не владеет, а в переводе уже не то. Да и не только в языке дело, культурный контекст нужен.
Вот если хочешь поделиться восторгами по поводу музыки, видом с горной вершины, невероятного здания, картины, скульптуры — можно показать близким и друзьям, и хоть в какой-то степени, но всё-таки оценят! А не оценят, так хоть заинтересуются...
Но есть такая очень важная для меня сторона жизни, где я своими восторгами я обычно не могу поделиться ни с кем из близких. Там происходят революции, там прямо при нас, прямо сегодня открывают новые континенты, а показать не могу, не могу поделиться.
Симон Анри в прошлом году придумал слабые модельные категории — это настолько круто, что учебники (конечно, не школьные) переписывать можно, он вообще на верном пути в ближайшее время доказать гипотезу Симпсона и вскультивировать целиком ландшафт этой науки. Эмили Риль — придумала принципиально новый подход к проблеме когерентности, красиво как симфония. Две недели назад Пит показал мне с коллегами Эвдоксовы вещественные числа — способ определить вещественные числа через квазиэндоморфизмы на абелевой группе целых. Харальд Хельфготт (тот самый мужик, который недавно слабую гипотезу Гольдбаха доказал, профессорствующий, кстати, у нас в Гёттингене) — оптимизировал решето Эратосфена просто невероятно круто. Это просто четыре рандомных вещи, но оно там такое всё, искрится как фейерверк и всё время что-то новое. Это так красиво, что дух захватывает, это окрыляет, этим хочется делиться, это хочется показывать. Но тот язык, на котором написана эта поэзия, к сожалению, не знает почти никто, и культурный контекст за вечер не перескажешь.
Кто-то в комментах:
Бы бы признателен за ссылки. Полагаю, не только я.
Куклев:
Оно всё гуглится элементарно:
Симон Анри и новое по части модельных категорий:
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://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/
Обзор менее часто употребимых схем рекурсии (вроде динаморфизма или дендроморфизма) с множеством ссылок на слайды, статьи, пейперы и видео. Если не знаете, чем себя занять на этих затянувшихся выходных — отличный вариант.
Обзор менее часто употребимых схем рекурсии (вроде динаморфизма или дендроморфизма) с множеством ссылок на слайды, статьи, пейперы и видео. Если не знаете, чем себя занять на этих затянувшихся выходных — отличный вариант.
Reddit
doloto's comment on "What are the hardest/most interesting, perhaps little known, but useful concepts that you know? I'm trying…
Explore this conversation and more from the haskell community
Math is your insurance policy: https://bartoszmilewski.com/2020/02/24/math-is-your-insurance-policy
Бартош неспешно рассказывает, почему нужно бросать натягивать CSS-шкурки на вордпресс и садиться изучать математику.
Бартош неспешно рассказывает, почему нужно бросать натягивать CSS-шкурки на вордпресс и садиться изучать математику.
Bartosz Milewski's Programming Cafe
Math is your insurance policy
We live in interesting times. For instance, we are witnessing several extinction events all at once. One of them is the massive extinction of species. The other is the extinction of jobs. Both are …
Прекрасный проект, вовсю эксплуатирующий (псевдо)полноту по Тьюрингу системы типов TypeScript. Есть даже решение задачи о N ферзях! Правда, натуральные числа кодируются вручную через словарь, так что данный проект умеет считать только до 10. Кодировка чисел Пеано может с этим помочь, но тогда автор упрётся в ограничение глубины рекурсии при выводе типов.
В любом случае, код хорошо документирован и достоен изучения:
https://github.com/ronami/meta-typing
В любом случае, код хорошо документирован и достоен изучения:
https://github.com/ronami/meta-typing
GitHub
GitHub - ronami/meta-typing: 📚 Functions and algorithms implemented purely with TypeScript's type system
📚 Functions and algorithms implemented purely with TypeScript's type system - ronami/meta-typing
Статья о функциональной архитектуре от Скотта Влашина:
https://increment.com/software-architecture/primer-on-functional-architecture
TL;DR: принципы функционального программирования — использование функций как основных строительных блоков, композиция, чистота — могут быть применены не только для решения тактических задач в прикладном коде, но и для построения более общей, стратегической картины решения целиком. Скотт Влашин в деталях описывает свой подход — построение крупномасштабных «функций»-воркфлоу, применение слоистой архитектуры (onion architecture), определение ограничений (boundaries) и использование событий как входных и выходных точек решения. В конце затрагивается тема функционального фронтэнда на примере Elm и рекламируется книга автора «Domain Modeling Made Functional».
https://increment.com/software-architecture/primer-on-functional-architecture
TL;DR: принципы функционального программирования — использование функций как основных строительных блоков, композиция, чистота — могут быть применены не только для решения тактических задач в прикладном коде, но и для построения более общей, стратегической картины решения целиком. Скотт Влашин в деталях описывает свой подход — построение крупномасштабных «функций»-воркфлоу, применение слоистой архитектуры (onion architecture), определение ограничений (boundaries) и использование событий как входных и выходных точек решения. В конце затрагивается тема функционального фронтэнда на примере Elm и рекламируется книга автора «Domain Modeling Made Functional».
Increment
A primer on functional architecture – Increment: Software Architecture
Approachable ideas and best practices to help engineering teams apply the principles of functional programming to high-level design and architecture.
Алехандро Серрано из 47 Degrees рассказывает, почему зависимые типы круто:
https://www.youtube.com/watch?v=JboZel47XU0
В пару к этому докладу хорошо идет доклад Виталия Брагилевского с f(by) о том, почему зависимые типы не круто:
https://www.youtube.com/watch?v=ohG-PRwOorA
¯\_(ツ)_/¯
https://www.youtube.com/watch?v=JboZel47XU0
В пару к этому докладу хорошо идет доклад Виталия Брагилевского с f(by) о том, почему зависимые типы не круто:
https://www.youtube.com/watch?v=ohG-PRwOorA
¯\_(ツ)_/¯
YouTube
Type-based formal verification - Alejandro Serrano
This talk provides an introduction to dependent and refinement types, and how they fit in the larger realm of formal verification.
Interested in learning more about 47 Degrees services around Functional Programming? Visit us at https://ww.47deg.com and follow…
Interested in learning more about 47 Degrees services around Functional Programming? Visit us at https://ww.47deg.com and follow…
Если вас задолбало, что вам присылают аудиосообщения там, где можно было обойтись текстом, есть замечательный вариант ответа:
https://vsychov.github.io/gif-generator
https://vsychov.github.io/gif-generator
Верификация корректности музыки с помощью системы типов:
https://www.infoq.com/articles/type-systems-verifying-musical-correctness
TL;DR: музыкальные композиции могут быть проверены с помощью системы типов, чтобы сделать негармоничные переходы между нотами непредставимыми. Для этого используется библиотека для хаскеля Mezzo и приводятся примеры с завтипами на идрисе. «Корректность» музыки вообще расплывчатый термин, поэтому в статье применяется дескриптивный подход — «если музыкальная тема отклоняется от ожидаемой модели, то это необычно» — и построение матрицы энтропии для различных комбинаций переходов от ноты к ноте.
https://www.infoq.com/articles/type-systems-verifying-musical-correctness
TL;DR: музыкальные композиции могут быть проверены с помощью системы типов, чтобы сделать негармоничные переходы между нотами непредставимыми. Для этого используется библиотека для хаскеля Mezzo и приводятся примеры с завтипами на идрисе. «Корректность» музыки вообще расплывчатый термин, поэтому в статье применяется дескриптивный подход — «если музыкальная тема отклоняется от ожидаемой модели, то это необычно» — и построение матрицы энтропии для различных комбинаций переходов от ноты к ноте.
InfoQ
It Ain't Necessarily So: Exploring Type Systems for Verifying Musical Correctness
Chris Ford explores what makes music correct and how we might encode it in a type system.
Опубликовал перевод статьи об истоках математической нотации из журнала Математической ассоциации Америки:
https://habr.com/ru/post/490520
Это четвертая статья из цикла, но именно она показалась мне наиболее интересной.
https://habr.com/ru/post/490520
Это четвертая статья из цикла, но именно она показалась мне наиболее интересной.
Смотрите, какой смешной мудачок:
https://twitter.com/fillpackart/status/1233629821286133761
https://twitter.com/fillpackart/status/1233629821286133761
Twitter
Tweet / Twitter
https://scalacenter.github.io/scala-developer-survey-2019 — результаты опроса от Scala Center за 2019 год подъехали.
Интересно, что Metals показал достаточно высокий процент использования! Это только укрепляет мою точку зрения, что за LSP будущее.
Интересно, что Metals показал достаточно высокий процент использования! Это только укрепляет мою точку зрения, что за LSP будущее.
https://www.reddit.com/r/typenoscript/comments/fda3pw/a_typelevel_lisp_interpreter_ish — интерпретатор лиспоподобного языка на типах TypeScript 🦾
Увы, из-за «Type instantiation is excessively deep and possibly infinite» максимум, что может — посчитать 4×4, а вот 5×5 уже нет.
Увы, из-за «Type instantiation is excessively deep and possibly infinite» максимум, что может — посчитать 4×4, а вот 5×5 уже нет.
Reddit
From the typenoscript community on Reddit
Explore this post and more from the typenoscript community
Немного личного.
В общем, что-то во мне надломилось и я решил уйти из TypeScript-коммьюнити. Старые библиотеки (если кому-то они нужны, лол) вроде fetcher-ts или circuit-breaker-monad буду поддерживать на уровне совместимости с мажорной версией fp-ts, но нового писать ничего не хочу — надоело бороться с ветряными мельницами. Ебитесь и дальше с «ехал
В течении ~полугода постараюсь конвертировать свой опыт (архитектура + фуллстэк-разработка + ПМ + девопс) под экосистему хаскеля. В идеале — найду проектного ментора и запилю несколько pet-проектов для портфолио.
Хотел написать, как всегда, «не переключайтесь», но именно сейчас то время, чтобы переключить канал. Этот тайпскриптер сломался, несите другого.
В общем, что-то во мне надломилось и я решил уйти из TypeScript-коммьюнити. Старые библиотеки (если кому-то они нужны, лол) вроде fetcher-ts или circuit-breaker-monad буду поддерживать на уровне совместимости с мажорной версией fp-ts, но нового писать ничего не хочу — надоело бороться с ветряными мельницами. Ебитесь и дальше с «ехал
any через any», но уже без меня ¯\_(ツ)_/¯В течении ~полугода постараюсь конвертировать свой опыт (архитектура + фуллстэк-разработка + ПМ + девопс) под экосистему хаскеля. В идеале — найду проектного ментора и запилю несколько pet-проектов для портфолио.
Хотел написать, как всегда, «не переключайтесь», но именно сейчас то время, чтобы переключить канал. Этот тайпскриптер сломался, несите другого.
GitHub
GitHub - YBogomolov/fetcher-ts: Type-safe wrapper around Fetch API
Type-safe wrapper around Fetch API. Contribute to YBogomolov/fetcher-ts development by creating an account on GitHub.