Telegram Web Link
In the #ECOOP23 paper 'Programming with Purity Reflection: Peaceful Coexistence of Effects, Laziness, and Parallelism,' we present a new programming construct that enables selective lazy and/or parallel evaluation.

In a nutshell, purity reflection enables a higher-order function to inspect the purity of a function argument and to vary its behavior based on this information.
For example, a function like Set.count can use parallel evaluation when given a pure predicate and revert to sequential evaluation when given an impure predicate.

The full paper is available here: https://drops-beta.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.18

You can read more about purity reflection in Flix here: https://doc.flix.dev/purity-reflection.html
MacoCaml: Staging Composable and Compilable Macros
N. Xie, L. White, O. Nicole, J. Yallop

We introduce MacoCaml, a new design and implementation of compile-time code generation for the OCaml language. MacoCaml features a novel combination of macros with phase separation and quotation-based staging, where macros are considered as compile-time bindings, expression cross evaluation phases using staging annotations, and compile-time evaluation happens inside top-level splices. We provide a theoretical foundation for MacoCaml by formalizing a typed source calculus 𝑚𝑎𝑐𝑜 that supports interleaving typing and compile-time code generation, references with explicit compile-time heaps, and modules. We study various crucial properties including soundness and phase distinction. We have implemented MacoCaml in the OCaml compiler, and ported two substantial existing libraries to validate our implementation.

https://xnning.github.io/papers/icfp23.pdf
The First Room-Temperature Ambient-Pressure Superconductor

https://arxiv.org/abs/2307.12008

Воспроизведения пока нет, но на данный момент звучит и выглядит достаточно правдоподобно.
Forwarded from Web to Album
Looking for some interesting summer reading? JFP has just published the latest batch of PhD abstracts for your reading pleasure, with links to the full dissertations. https://www.cambridge.org/core/journals/journal-of-functional-programming/article/phd-abstracts/A32EE036508B4F3B309230D342DA7C2C source
https://arxiv.org/abs/2308.08347

Continuing WebAssembly with Effect Handlers
L. Phipps-Costin, A. Rossberg, A. Guha, D. Leijen, D. Hillerström, KC Sivaramakrishnan, S. Lindley
Lectures on applied category theory
John Baez

https://math.ucr.edu/home/baez/act_course/
Understanding Random Forests: From Theory to Practice, thesis
G. Louppe

https://arxiv.org/abs/1407.7502
Grokking as Compression: A Nonlinear Complexity Perspective
Z. Liu, Z. Zhong, M. Tegmark

https://arxiv.org/abs/2310.05918
Quotient Haskell, Lightweight Quotient Types for All
B. Hewer, G. Hutton

Subtypes and quotient types are dual type abstractions. However, while subtypes are widely used both explicitly and implicitly, quotient types have not seen much practical use outside of proof assistants. A key difficulty to wider adoption of quotient types lies in the significant burden of proof-obligations that arises from their use. In this article, we address this issue by introducing a class of quotient types for which the proof-obligations are decidable by an SMT solver. We demonstrate this idea in practice by presenting Quotient Haskell, an extension of Liquid Haskell with support for quotient types.

https://www.cs.nott.ac.uk/~pszgmh/quotient-haskell.pdf
Capturing Types

https://dl.acm.org/doi/abs/10.1145/3618003

Type systems usually characterize the shape of values but not their free variables. However, many desirable safety properties
could be guaranteed if one knew the free variables captured by values. We describe CC<:□ , a calculus where such captured
variables are succinctly represented in types, and show it can be used to safely implement efects and efect polymorphism via
scoped capabilities. We discuss how the decision to track captured variables guides key aspects of the calculus, and show that
CC<:□ admits simple and intuitive types for common data structures and their typical usage patterns. We demonstrate how
these ideas can be used to guide the implementation of capture checking in a practical programming language.
Forwarded from ∫f(x)dx
Пародийная песня "The Telnet Song" за авторством Guy Steele была опубликована в Communications of the ACM в апреле 1984 года:
https://dl.acm.org/doi/pdf/10.1145/358027.1035691
2025/07/05 17:15:17
Back to Top
HTML Embed Code: