Любопытный пейпер: «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://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.»
GitHub
GitHub - matijapretnar/aeff: An interactive interpreter for asynchronous algebraic effects
An interactive interpreter for asynchronous algebraic effects - matijapretnar/aeff
Ко мне продолжают приходить в личку с вопросами о продолжении стримов по ФП. Видимо, нельзя просто так вот уйти из коммьюнити.
Так что оставайтесь дома и приходите сегодня в 20:00 на стрим по функциональному TypeScript. Рассмотрим паттерн тайпкласса и некоторые простые тайпклассы — Eq, Ord, Functor, Monad, Traversable, etc.
https://youtu.be/pPUguhBZ8JY
Так что оставайтесь дома и приходите сегодня в 20:00 на стрим по функциональному TypeScript. Рассмотрим паттерн тайпкласса и некоторые простые тайпклассы — Eq, Ord, Functor, Monad, Traversable, etc.
https://youtu.be/pPUguhBZ8JY
YouTube
Функциональный TypeScript: паттерн тайпкласса
Поговорим о реализации паттерна тайпкласса в функциональном TypeScript и рассмотрим некоторые полезные тайпклассы.
Статья «Lightweight highker-kinded polymorphism»: https://www.cl.cam.ac.uk/~jdy22/papers/lightweight-higher-kinded-polymorphism.pdf
Код из…
Статья «Lightweight highker-kinded polymorphism»: https://www.cl.cam.ac.uk/~jdy22/papers/lightweight-higher-kinded-polymorphism.pdf
Код из…
Бесплатная книга: «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.
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://www.youtube.com/watch?v=FeG41moU8Xk
YouTube
Bartosz Milewsky & Oli Makhasoeva - Recursion schemes, categorically!
Recursion schemes are an example of the direct application of category theory to programming. Category theory uses diagrams to define functors, algebras, and universal constructions. Wondering about how to make connections between the most abstract branch…
Волны твиттера принесли прекрасное: https://twitter.com/vamchale/status/1249076951685398530
TL;DR: в Elm была проблема — паттерн-матчинг по негативным числовым литералам приводил к ошибке парсинга. Эван Чаплицкий не только не исправил этот баг (при этом спросив у автора тикета «Instead of fake examples, can you explain how this comes up?») — он еще и добавил в компилятор текст ошибки, который предлагает использовать вместо паттерн-матчинга if-else.
TL;DR: в Elm была проблема — паттерн-матчинг по негативным числовым литералам приводил к ошибке парсинга. Эван Чаплицкий не только не исправил этот баг (при этом спросив у автора тикета «Instead of fake examples, can you explain how this comes up?») — он еще и добавил в компилятор текст ошибки, который предлагает использовать вместо паттерн-матчинга if-else.
Twitter
Vanessa McHale
- pattern matching on literals hits a parser bug in elm - someone reports this - evan responds by saying "Why are you doing this? Instead of fake examples, can you explain how this comes up?" (not kidding) github.com/elm/compiler/i…
Грант Сандерсон — автор прекраснейшего канала 3Blue1Brown, на который я рекомендую подписаться, — о причинах, почему люди вообще занимаются математикой:
https://www.youtube.com/watch?v=s_L-fp8gDzY
https://www.youtube.com/watch?v=s_L-fp8gDzY
YouTube
What Makes People Engage With Math | Grant Sanderson | TEDxBerkeley
Grant Sanderson (@3blue1brown) is the founder of the math outreach and education YouTube channel 3blue1brown, which has over two million subscribers and over 85 million total views. He’s collaborated with many other online educators, such as MinutePhysics…
Достаточно интересный пейпер от Андрея Мохова, Нила Митчела и Саймона Пейтона Джонса о системах сборки (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
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
Cambridge Core
Build systems à la carte: Theory and practice | Journal of Functional Programming | Cambridge Core
Build systems à la carte: Theory and practice - Volume 30
Собрал небольшую подборку видео о программировании на 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».
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».