https://arxiv.org/abs/2203.15426 Dal Lago, Gavazzo, Ghyselen, [2022] "On Reinforcement Learning, Effect Handlers, and the State Monad"

We study the algebraic effects and handlers as a way to support decision-making abstractions in functional programs, whereas a user can ask a learning algorithm to resolve choices without implementing the underlying selection mechanism, and give a feedback by way of rewards. Differently from some recently proposed approach to the problem based on the selection monad [Abadi and Plotkin, LICS 2021], we express the underlying intelligence as a reinforcement learning algorithm implemented as a set of handlers for some of these algebraic operations, including those for choices and rewards. We show how we can in practice use algebraic operations and handlers -- as available in the programming language EFF -- to clearly separate the learning algorithm from its environment, thus allowing for a good level of modularity. We then show how the host language can be taken as a lambda-calculus with handlers, this way showing what the essential linguistic features are. We conclude by hinting at how type and effect systems could ensure safety properties, at the same time pointing at some directions for further work.

“CoqQ: Foundational Verification of Quantum Programs”

Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying (2022)

https://arxiv.org/abs/2207.11350

CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic for proving properties of programs. CoqQ is foundational: the program logic is formally proved sound with respect to a denotational semantics based on state-of-art mathematical libraries (mathcomp and mathcomp analysis). CoqQ is also practical: assertions can use Dirac expressions, which eases concise specifications, and proofs can exploit local and parallel reasoning, which minimizes verification effort. We illustrate the applicability of CoqQ with many examples from the literature.

#coq #quantum_programming

Эта небольшая заметка посвящена нескольким новостям по нашей тематике.

Во-первых, хочу напомнить, что в июне прошла конференция PLDI 2022 и многие из представленных там работ имеют компиляторную тематику. Вот программа конференции: https://pldi22.sigplan.org/program/program-pldi-2022/

Во-вторых, давайте поговорим о весьма достойных книгах, которые официально только готовятся к печати и выйдут в 2022-2023 гг.

Нас ждет третье издание классики Engineering a Compiler. Второе издание вышло в 2012 году и мне, увы, пока не удалось установить, в чем же особенности нового издания. Судя по всему, новая версия знаменитого учебника выйдет в этом сентябре: https://www.amazon.com/Engineering-Compiler-Keith-D-Cooper/dp/0128154128

В феврале 2023 года выйдет Essentials of Compilation в издательстве MIT: https://mitpress.mit.edu/books/essentials-compilation Материал в разных редакциях давно уже публиковался на github: https://github.com/IUCompilerCourse/Essentials-of-Compilation

Еще одна довольно известная онлайн-книга скоро будет напечатана. Речь об SSA Book. Официально она теперь называется SSA-based Compiler Design: https://link.springer.com/book/9783030805142 Ждем ее ближе к февралю 2023 года.

Наконец, упомяну о настоящем "долгострое": новой версии классики Programming Languages: An Interpreter-Based Approach" от Samuel Kamin. Новый автор и известный компьютерный ученый, Norman Ramsey, работал над своей версией еще, кажется, с 2005 года. На протяжении многих лет черновые варианты учебника адресно рассылались отдельным профессорам в разных университетах. И, вот, наконец, в этом октябре книга под официальным названием Programming Languages Build, Prove, and Compare будет напечатана: https://www.cambridge.org/ru/academic/subjects/computer-science/programming-languages-and-applied-logic/programming-languages-build-prove-and-compare

Good overview of some entertaining stuff, by Xavier Leroy: https://xavierleroy.org/CdF/2018-2019/

Other courses are good as well (though the presentation is usually more deep/technical):
- https://xavierleroy.org/CdF/2020-2021/
- https://xavierleroy.org/CdF/2019-2020/
- https://xavierleroy.org/mpri/2-4/
- other materials at https://xavierleroy.org/teaching.html

Mathematical Proof Between Generations

https://arxiv.org/pdf/2207.04779.pdf

A Formalization of SQL with Nulls (Wilmer Ricciotti, James Cheney):

https://cs.paperswithcode.com/paper/a-formalization-of-sql-with-nulls

> SQL is the world's most popular declarative language, forming the basis of the multi-billion-dollar database industry. Although SQL has been standardized, the full standard is based on ambiguous natural language rather than formal specification. Commercial SQL implementations interpret the standard in different ways, so that, given the same input data, the same query can yield different results depending on the SQL system it is run on. Even for a particular system, mechanically checked formalization of all widely-used features of SQL remains an open problem. The lack of a well-understood formal semantics makes it very difficult to validate the soundness of database implementations. Although formal semantics for fragments of SQL were designed in the past, they usually did not support set and bag operations, lateral joins, nested subqueries, and, crucially, null values. Null values complicate SQL's semantics in profound ways analogous to null pointers or side-effects in other programming languages. Since certain SQL queries are equivalent in the absence of null values, but produce different results when applied to tables containing incomplete data, semantics which ignore null values are able to prove query equivalences that are unsound in realistic databases. A formal semantics of SQL supporting all the aforementioned features was only proposed recently. In this paper, we report about our mechanization of SQL semantics covering set/bag operations, lateral joins, nested subqueries, and nulls, written in the Coq proof assistant, and describe the validation of key metatheoretic properties. Additionally, we are able to use the same framework to formalize the semantics of a flat relational calculus (with null values), and show a certified translation of its normal forms into SQL.

An assortment of curious mathematical pieces.

A la POPLOG: https://kam.mff.cuni.cz/~matousek/stml-53-matousek-1.pdf

https://www.youtube.com/watch?v=Q61dh87WGrE

Demos of projectional editors for functional languages: Lamdu, Dark, Hazel, tylr and Lisperanto. Also a link to the whole meetup video is in the description.

https://shark.fish/curiosity

If you have nothing to do for the next couple of hours. Or just bored at your work. 😁

https://ai.googleblog.com/2022/07/ml-enhanced-code-completion-improves.html

Google combines Machine-Learned Transformer-based code completions with "traditional" semantic analysis-based completions and checks and measures some productivity improvements.

It's nice to be Google: you can have 10k+ devs in your treatment group and the rest of Google in control.

https://www.youtube.com/watch?v=BzuEGdGHKjc

Julia developers be like
What if use LLVM as a JIT compiler but unironically? And also have macros to implement staged compilation right in Julia and then JIT what's left? We'll implement blazing fast autodiff and put everything in a GPU!

Python developers at Google be like
Wait we have our own compiler to, XLA! And we can write Python functions to specialize other Python functions, right? We too can implement blazing bast autodiff and even target TPUs!

Actually JAX's approach to compiling Python to IR with tracing right inside Python is pretty fascinating. They also gain and exploit Futamura projection-like functionality to make (almost) everything composable. Clever stuff.

https://medium.com/@kentbeck_7670/test-commit-revert-870bbd756864

Kent Beck promotes another crazy radical workflow. But it might indeed be fun to try for a hobby project. 😊

Я начинаю выкатывать первую итерацию блогпоста по истории ФП, надеюсь что у кого-нибудь будут какие-то замечания по первой главе
токо осторожно, там до первой главки по истории идет метаисторический выблев на пять экранов
https://gist.github.com/klapaucius/f0adec8a567b7bf000c8bcf99686a9bd

Вас в школе учитель(ница) математики заставляла расписывать промежуточные шаги при решении задачи? Исследователи из Google AI заставили это делать свои Language Models:
https://ai.googleblog.com/2022/05/language-models-perform-reasoning-via.html

Удивительное дело, но явное выписывание промежуточных шагов сильно помогает решать математические задачки. Видимо, учителя математики что-то нащупали за последние 200 лет своей совокупной деятельности.

Что несколько более удивительно, обучение модели выполнению детерминированных логических шагов, в частности, арифметических операций происходит прямо на естественном языке, натурально как в школе. Точнее, людям в школе-то как раз дают явные алгоритмы сложения-вычитания-умножения-деления ("в столбик"), а "ИИ" (уже/пока что) — нет.

Но исследователи и исследовательницы на этом не остановились, и подумали "а что если заменить шаги математических вычислений на манипуляции, производимые роботом?":
https://ai.googleblog.com/2022/08/towards-helpful-robots-grounding.html

Оказалось, что докинув в замес ещё пару ML/RL-трюков (image-based behavioral cloning, temporal-difference-based RL, RetinaGAN и прочее по мелочи) можно поднять процент успешных задуманных "хитрых планов" до 84, и выполненных до 74. Ещё недостаточно хорошо, чтобы "спасать жизни", но сильно лучше, чем 50/50.

По такой радости даже запилили "продающий сайт":
https://sites.research.google/palm-saycan

следующая глава
https://gist.github.com/klapaucius/f0adec8a567b7bf000c8bcf99686a9bd#%D0%BF%D1%81%D0%B5%D0%B2%D0%B4%D0%BEcpl