Denotational design with type class morphisms

Conal Elliott

Type classes provide a mechanism for varied implementations of standard interfaces. Many of these interfaces are founded in mathematical tradition and so have regularity not only of types but also of properties (laws) that must hold. Types and properties give strong guidance to the library implementor, while leaving freedom as well. Some of this remaining freedom is in how the implementation works, and some is in what it accomplishes.

To give additional guidance to the what, without impinging on the how, this paper proposes a principle of type class morphisms (TCMs), which further refines the compositional style of denotational semantics. The TCM idea is simply that the instance’s meaning is the meaning’s instance. This principle determines the meaning of each type class instance, and hence defines correctness of implementation. It also serves to transfer laws about a type’s semantic model, such as the class laws, to hold for the type itself. In some cases, it also provides a systematic guide to implementation, and in some cases, valuable design feedback.

The paper is illustrated with several examples of types, meanings, and morphisms.

http://conal.net/papers/type-class-morphisms/

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

A brief overview of two new features for "OCaml 6.0" that Jane Street is finalizing.

The first one is unboxed types with "levity polymorphism" (more or less) and stack allocation.

Safe stack allocation requires tracking values that don't escape scope (and scope inference) which largely amounts to linearity. This leads to the second feature: race-free parallel (concurrent) programming.

Apparently, it requires tracking more properties than just linearity, but once you've added kinds and modes to your type system, it's hard to stop half-way... 😁

Harnessing the Universal Geometry of Embeddings

We present the first method to translate text embeddings across different spaces without any paired data or encoders.
Our method, vec2vec, reveals that all encoders—regardless of architecture or training data—learn nearly the same representations!
We demonstrate how to translate between these black-box embeddings without any paired data, maintaining high fidelity.
Using vec2vec, we show that vector databases reveal (almost) as much as their inputs.
Given just vectors (e.g., from a compromised vector database), we show that an adversary can extract sensitive information (e.g., PII) about the underlying text.

Strong Platonic Representation Hypothesis (S-PRH)
We thus strengthen Huh et al.'s PRH to say:
The universal latent structure of text representations can be learned and harnessed to translate representations from one space to another without any paired data or encoders.

https://arxiv.org/abs/2505.12540

Unpublished lecture notes in a secret place. All those moments will be lost in time, like tears in rain. Enjoy!

https://www.cs.cmu.edu/~rwh/courses/atpl/pdfs/

Scalable Pattern Matching in Computation Graphs

Luca Mondada
Pablo Andrés-Martínez

Graph rewriting is a popular tool for the optimisation and modification of graph expressions in domains such as compilers, machine learning and quantum computing. The underlying data structures are often port graphs—graphs with labels at edge endpoints. A pre-requisite for graph rewriting is the ability to find graph patterns. We propose a new solution to pattern matching in port graphs. Its novelty lies in the use of a pre-computed data structure that makes the pattern matching runtime complexity independent of the number of patterns. This offers a significant advantage over existing solutions for use cases with large sets of small patterns.

Our approach is particularly well-suited for quantum superoptimisation. We provide an implementation and benchmarks showing that our algorithm offers a 20x speedup over current implementations on a dataset of 10000 real world patterns describing quantum circuits.

https://arxiv.org/abs/2402.13065

https://www.youtube.com/@currentcontinuation тяп-подкаст

1. Destabilizing Iris (https://doi.org/10.1145/3729284)

2. Tree Borrows (https://doi.org/10.1145/3735592)

3. Principal Type Inference under a Prefix: A Fresh Look at Static Overloading (https://doi.org/10.1145/3729308)

4. Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic (https://doi.org/10.1145/3729246)

5. Practical Type Inference with Levels (https://doi.org/10.1145/3729338)

6. AWDIT: An Optimal Weak Database Isolation Tester (https://doi.org/10.1145/3742465)

Compiling Untyped Lambda Calculus to Lower-Level Code by Game Semantics and Partial Evaluation

Daniil Berezun
Neil D. Jones

Any expression M in ULC (the untyped λ-calculus) can be compiled into a rather low-level language we call LLL, whose programs contain none of the traditional implementation devices for functional languages: environments, thunks, closures, etc. A compiled program is first-order functional and has a fixed set of working variables, whose number is independent of M. The generated LLL code in effect traverses the subexpressions of M.

We apply the techniques of game semantics to the untyped λcalculus, but take a more operational viewpoint that uses less mathematical machinery than traditional presentations of game semantics. Further, the untyped lambda calculus ULC is compiled into LLL by partially evaluating a traversal algorithm for ULC.

https://dl.acm.org/doi/10.1145/3018882.3020004

Learn you Galois Fields for Great Good

https://xorvoid.com/galois_fields_for_great_good_00.html

Fail Faster: Staging and Fast Randomness for High-Performance PBT

property-based testing - ✅
staging - ✅

https://arxiv.org/abs/2503.19797

video: https://www.youtube.com/watch?v=ux49IvxKQR8

OPLSS 2025

https://www.cs.uoregon.edu/research/summerschool/summer25/topics.php

Functional abstract interpretation

Sebastian Graf

In this thesis, I present two results of my work to improve GHC: the first is a static analysis for pattern-match coverage checking that is both more efficient and more precise than the state of the art; the second is a design pattern for deriving static higher-order analyses and dynamic semantics alike from a generic denotational interpreter, in order to share intuition and correctness proofs. This design pattern generalises Cousot’s seminal work on trace-based abstract interpretation to higher-order analyses such as GHC’s Demand Analysis.

https://simon.peytonjones.org/abs-den/

Dual-Numbers Reverse AD for Functional Array Languages
T. Smelding, M. Konarski, S. PJ, A. Fitzgibbon

https://arxiv.org/abs/2507.12640