Latent Effects for Reusable Language Components

https://arxiv.org/abs/2108.11155

https://doi.org/10.1017/S0956796821000113
"How to design co-programs" by Jeremy Gibbons

Статья призывает расширить подход How to Design Programs (aka HtDP, серия курсов, обучающих студентов программированию с нуля, плюс два издания одноимённой книги: https://htdp.org/ если кто не знает) за счёт введения понятия ко-рекурсивных функций и соответствующих паттернов для их построения.

Говоря по-простому, ко-рекурсивные функции — это такие, которые строят свой результат "по кусочкам", используя конструкторы соответствующего (алгебраического) типа данных, вместо того (или вместе с тем) чтобы разбирать входные данные "на кусочки" при помощи сопоставления с образцом (aka [datatype] pattern matching).

Я безусловно согласен с Гиббонсом в том, что ко-рекурсивные функции — очень полезный инструмент в арсенале разработчика, особенно, начинающего. Тем не менее, на мой взгляд, эта тема требует намного более тщательной методической проработки чтобы органично встроиться в общую канву HtDP.

Более того, самая интересная часть этой статьи — ещё одна статья, которая не была написана, к сожалению. 😊 В середине повествования Гиббонс обсуждает "генеративную рекурсию" (generative recursion, термин из HtDP), и показывает как функции (изначально) в форме общей генеративной рекурсии могут быть представлены в виде композиции структурно-рекурсивной и ко-рекурсивной функции (так же известной как "иломорфизм" или "хиломорфизм" — hylomorphism). К сожалению, за кадром остаются самые важные и интересные вопросы: как понять, что данную конкретную функцию можно представить в виде такой композиции, или придётся использовать генеративную рекурсию общего вида? как выбрать подходящую промежуточную структуру для рекурсии и ко-рекурсии? Возможно, эти вопросы удастся прояснить тем, кто интегрирует тему ко-рекурсивных функций в свои учебные программы. 😊

Stainless: Home
https://stainless.epfl.ch/

https://arxiv.org/abs/2003.03021 Jia, Rinard, [2021] "Exploiting Verified Neural Networks via Floating Point Numerical Error"

https://ajrouvoet.github.io/files/thesis.pdf Rouvoet, [2021] "Correct by Construction Language Implementations"

Thursday 7.10 at 18:30 Matthieu Sozeau is giving an online talk on MetaCoq: https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html. Should be interesting 😊

7го еще кстати будет https://www.youtube.com/watch?v=p9ANNglWMvc

Exciting (promising or provocative) upcoming talks from SPLASH'21:

https://conf.researchr.org/details/aplas-2021/aplas-2021-keynote-talks/1/-Solidifying-and-Advancing-the-Software-Foundations

https://conf.researchr.org/details/sas-2021/sas-2021-papers/4/Exploiting-Verified-Neural-Networks-via-Floating-Point-Numerical-Error (trollface)

https://conf.researchr.org/details/sle-2021/sle-2021-papers/15/SLE-Keynote-Integrating-Usability-into-Programming-Language-Design (finally something tangible on programming languages ease of use?)

https://conf.researchr.org/details/sle-2021/sle-2021-papers/8/Vision-The-Next-700-Language-Workbenches (will we finally get people actually using Language Workbenches at scale? 😃)

https://conf.researchr.org/details/aplas-2021/aplas-2021-papers/11/A-compilation-method-for-dynamic-typing-in-ML (a Standard ML modernization at last! 😂 Actually the authors talk about native compilation of dynamic types along with static types which is interesting.)

https://conf.researchr.org/details/gpce-2021/gpcegpce+2021+-+20th+international+conference+on+generative+programming%3A+concepts+%26+experiences2021/3/A-Variational-Database-Management-System

https://conf.researchr.org/details/gpce-2021/gpcegpce+2021+-+20th+international+conference+on+generative+programming%3A+concepts+%26+experiences2021/13/On-Stack-Replacement-for-Program-Generators-and-Source-to-Source-Compilers (on-stack replacement as a source-level program transformation... sounds simple! 😂)

https://2021.splashcon.org/details/splash-2021-rebase/4/A-Retrospective-on-the-Design-of-the-Swift-Programming-Language (Swift is already so old they're doing a retrospective on it! 😱)

https://2021.splashcon.org/details/splash-2021-oopsla/6/Efficient-Compilation-of-Algebraic-Effect-Handlers

https://2021.splashcon.org/details/splash-2021-Onward-papers/4/Language-guided-Programming (the promise of natural language programming never gets old 😏)

https://2021.splashcon.org/details/splash-2021-Onward-Essays/2/Programming-as-Architecture-Design-and-Urban-Planning

https://2021.splashcon.org/details/splash-2021-splash-keynotes/1/Integrated-Scientific-Modeling-and-Lab-Automation (I suspect Cardelli will tell the same story as before but it's so fascinating! 😃)

https://2021.splashcon.org/details/splash-2021-oopsla/30/Gradually-Structured-Data

https://2021.splashcon.org/details/splash-2021-oopsla/27/Well-Typed-Programs-Can-Go-Wrong-A-Study-of-Typing-Related-Bugs-in-JVM-Compilers (trollface)

https://2021.splashcon.org/details/splash-2021-oopsla/59/How-Statically-Typed-Functional-Programmers-Write-Code (I was one of the subjects so it's interesting what they infer 😃)

https://2021.splashcon.org/details/agere-2021-papers/3/Session-Types-in-Elixir (Exactly what Elixir programmers were missing! 😁)

https://2021.splashcon.org/details/rebls-2021-papers/1/ShapeRank-Rank-Polymorphism-meets-Reactive-Streams (APL punks not dead!)

https://2021.splashcon.org/details/vmil-2021-papers/6/Reflections-on-a-decade-of-MoarVM-a-runtime-for-the-Raku-programming-language (Ever heard of Raku? Perl 6 maybe? And they're doing some interesting stuff...)

https://2021.splashcon.org/details/hatra-2021-papers/10/User-driven-design-and-evaluation-of-Liquid-Types-in-Java (Do Java users need Liquid Types? Indeed... 😁)

https://2021.splashcon.org/details/splash-2021-recent-sigplan/22/Reasoning-about-the-Garden-of-Forking-Paths (We'll finally be able to reason about computational complexity of lazy programs. In Coq! 😈)

https://2021.splashcon.org/details/splash-2021-recent-sigplan/71/Python-3-Types-in-the-Wild-A-Tale-of-Two-Type-Systems ("Surprisingly, when developers use static types, the code rarely type-checks..." Surprisingly? 🤔)

The recordings of TLA+ Conf 2021 (including Q&A) are now online at
https://www.youtube.com/watch?v=QKCG3tz4mOU&list=PLWLcqZLzY8u9kzmWgs3HPRm3Cw85LTpD2