arXiv subjects

Gabriel Scherer

Publications and source records attributed to Gabriel Scherer.

At least 19 recordsLinked to original sources

arXiv2026

How to benchmark: the Measure-Explain-Test-Improve loop

I would like to share recommendations on how to do performance benchmarks for the purpose of computer science research evaluation. Research in my field (programming language research) often involves performance considerations, but it is typically not the main tool used to evaluate our research (typically we evaluate via formal statements and their proofs, experience writing large or interesting examples, or systematic comparison of expressivity, feature set, etc.). My impression is that, as a result, we tend to not do our performance evaluation very well. In the present document I will try to explain a methodology to do benchmarking correctly (I hope!). People with no former benchmarking experience should be able to build solid performance evaluation as part of their research. I explain the justification for each aspect along the way.

cs.PL↗

arXiv2025

Omnidirectional type inference for ML: principality any way

The Damas-Hindley-Milner (ML) type system owes its success to principality, the property that every well-typed expression has a unique most general type. This makes inference predictable and efficient. Unfortunately, many extensions of ML (GADTs, higher-rank polymorphism, and static overloading) endanger princpality by introducing _fragile_ constructs that resist principal inference. Existing approaches recover principality through directional inference algorithms, which propagate _known_ type information in a fixed (or static) order (e.g. as in bidirectional typing) to disambiguate such constructs. However, the rigidity of a static inference order often causes otherwise well-typed programs to be rejected. We propose _omnidirectional_ type inference, where type information flows in a dynamic order. Typing constraints may be solved in any order, suspending when progress requires known type information and resuming once it becomes available, using _suspended match constraints_. This approach is straightforward for simply typed systems, but extending it to ML is challenging due to let-generalization. Existing ML inference algorithms type let-bindings (let x = e1 in e2) in a fixed order: type e1, generalize its type, and then type e2. To overcome this, we introduce _incremental instantiation_, allowing partially solved type schemes containing suspended constraints to be instantiated, with a mechanism to incrementally update instances as the scheme is refined. Omnidirectionality provides a general framework for restoring principality in the presence of fragile features. We demonstrate its versatility on two fundamentally different features of OCaml: static overloading of record labels and datatype constructors and semi-explicit first-class polymorphism. In both cases, we obtain a principal type inference algorithm that is more expressive than OCaml's current typechecker.

cs.PL↗

arXiv2025

The free bifibration on a functor

We consider the problem of constructing the free bifibration generated by a functor of categories $p : D \to C$. This problem was previously considered by Lamarche, and is closely related to the problem, considered by Dawson, Par\'e, and Pronk, of ``freely adjoining adjoints'' to a category. We develop a proof-theoretic approach to the problem, beginning with a construction of the free bifibration $\Lambda_p : Bifib(p)\to C$ in which objects of $Bifib(p)$ are formulas of a primitive ``bifibrational logic'', and arrows are derivations in a cut-free sequent calculus modulo a notion of permutation equivalence. We show that instantiating the construction to the identity functor generates a _zigzag double category_ $\mathbb{Z}(C)$, which is also the free double category with companions and conjoints (or fibrant double category) on $C$. The approach adapts smoothly to the more general task of building $(P,N)$-fibrations, where one only asks for pushforwards along arrows in $P$ and pullbacks along arrows in $N$ for some subsets of arrows; this encompasses Kock and Joyal's notion of _ambifibration_ when $(P,N)$ form a factorization system. We establish a series of progressively stronger normal forms, guided by ideas of _focusing_ from proof theory, and obtain a canonicity result under assumption that the base category is factorization preordered relative to $P$ and $N$. This canonicity result allows us to decide the word problem and to enumerate relative homsets without duplicates. Finally, we describe several examples of a combinatorial nature, including a category of plane trees generated as a free bifibration over $\omega$, and a category of increasing forests generated as a free ambifibration over $\Delta$, which contains the lattices of noncrossing partitions as quotients of its fibers by the Beck-Chevalley condition for bicartesian squares.

math.CT↗

arXiv2024

Tail Modulo Cons, OCaml, and Relational Separation Logic

Common functional languages incentivize tail-recursive functions, as opposed to general recursive functions that consume stack space and may not scale to large inputs. This distinction occasionally requires writing functions in a tail-recursive style that may be more complex and slower than the natural, non-tail-recursive definition. This work describes our implementation of the *tail modulo constructor* (TMC) transformation in the OCaml compiler, an optimization that provides stack-efficiency for a larger class of functions -- tail-recursive *modulo constructors* -- which includes in particular the natural definition of `List.map` and many similar recursive data-constructing functions. We prove the correctness of this program transformation in a simplified setting -- a small untyped calculus -- that captures the salient aspects of the OCaml implementation. Our proof is mechanized in the Coq proof assistant, using the Iris base logic. An independent contribution of our work is an extension of the Simuliris approach to define simulation relations that support different calling conventions. To our knowledge, this is the first use of Simuliris to prove the correctness of a compiler transformation.

cs.PL↗

arXiv2023

Unboxed data constructors -- or, how cpp decides a halting problem

We propose a new language feature for ML-family languages, the ability to selectively unbox certain data constructors, so that their runtime representation gets compiled away to just the identity on their argument. Unboxing must be statically rejected when it could introduce confusions, that is, distinct values with the same representation. We discuss the use-case of big numbers, where unboxing allows to write code that is both efficient and safe, replacing either a safe but slow version or a fast but unsafe version. We explain the static analysis necessary to reject incorrect unboxing requests. We present our prototype implementation of this feature for the OCaml programming language, discuss several design choices and the interaction with advanced features such as Guarded Algebraic Datatypes. Our static analysis requires expanding type definitions in type expressions, which is not necessarily normalizing in presence of recursive type definitions. In other words, we must decide normalization of terms in the first-order lambda-calculus with recursion. We provide an algorithm to detect non-termination on-the-fly during reduction, with proofs of correctness and completeness. Our termination-monitoring algorithm turns out to be closely related to the normalization strategy for macro expansion in the `cpp` preprocessor.

cs.PL↗

arXiv2023

Coqlex: Generating Formally Verified Lexers

A compiler consists of a sequence of phases going from lexical analysis to code generation. Ideally, the formal verification of a compiler should include the formal verification of each component of the tool-chain. An example is the CompCert project, a formally verified C compiler, that comes with associated tools and proofs that allow to formally verify most of those components. However, some components, in particular the lexer, remain unverified. In fact, the lexer of Compcert is generated using OCamllex, a lex-like OCaml lexer generator that produces lexers from a set of regular expressions with associated semantic actions. Even though there exist various approaches, like CakeML or Verbatim++, to write verified lexers, they all have only limited practical applicability. In order to contribute to the end-to-end verification of compilers, we implemented a generator of verified lexers whose usage is similar to OCamllex. Our software, called Coqlex, reads a lexer specification and generates a lexer equipped with a Coq proof of its correctness. It provides a formally verified implementation of most features of standard, unverified lexer generators. The conclusions of our work are two-fold: Firstly, verified lexers gain to follow a user experience similar to lex/flex or OCamllex, with a domain-specific syntax to write lexers comfortably. This introduces a small gap between the written artifact and the verified lexer, but our design minimizes this gap and makes it practical to review the generated lexer. The user remains able to prove further properties of their lexer. Secondly, it is possible to combine simplicity and decent performance. Our implementation approach that uses Brzozowski derivatives is noticeably simpler than the previous work in Verbatim++ that tries to generate a deterministic finite automaton (DFA) ahead of time, and it is also noticeably faster thanks to careful design choices. We wrote several example lexers that suggest that the convenience of using Coqlex is close to that of standard verified generators, in particular, OCamllex. We used Coqlex in an industrial project to implement a verified lexer of Ada. This lexer is part of a tool to optimize safety-critical programs, some of which are very large. This experience confirmed that Coqlex is usable in practice, and in particular that its performance is good enough. Finally, we performed detailed performance comparisons between Coqlex, OCamllex, and Verbatim++. Verbatim++ is the state-of-the-art tool for verified lexers in Coq, and the performance of its lexer was carefully optimized in previous work by Egolf and al. (2022). Our results suggest that Coqlex is two orders of magnitude slower than OCamllex, but two orders of magnitude faster than Verbatim++. Verified compilers and other language-processing tools are becoming important tools for safety-critical or security-critical applications. They provide trust and replace more costly approaches to certification, such as manually reading the generated code. Verified lexers are a missing piece in several Coq-based verified compilers today. Coqlex comes with safety guarantees, and thus shows that it is possible to build formally verified front-ends.

cs.PL↗

arXiv2022

Debootstrapping without Archeology: Stacked Implementations in Camlboot

Context: It is common for programming languages that their reference implementation is implemented in the language itself. This requires a "bootstrap": a copy of a previous version of the implementation is provided along with the sources, to be able to run the implementation itself. Those bootstrap files are opaque binaries; they could contain bugs, or even malicious changes that could reproduce themselves when running the source version of the language implementation -- this is called the "trusting trust attack". For this reason, a collective project called Bootstrappable was launched in 2016 to remove those bootstraps, providing alternative build paths that do not rely on opaque binaries. Inquiry: Debootstrapping generally combines a mix of two approaches. The "archaeological" approach works by locating old versions of systems, or legacy alternative implementations, that do not need the bootstrap, and by preserving or restoring the ability to run them. The "tailored" approach re-implements a new, non-bootstrapped implementation of the system to debootstrap. Currently, the "tailored" approach is dominant for low-level system components (C, coreutils), and the "archaeological" approach is dominant among the few higher-level languages that were debootstrapped. Approach: We advocate for the benefits of "tailored" debootstrapping implementations of high-level languages. The new implementation needs not be production-ready, it suffices that it is able to run the reference implementation correctly. We argue that this is feasible with a reasonable development effort, with several side benefits besides debootstrapping. Knowledge: We propose a specific design of composing/stacking several implementations: a reference interpreter for the language of interest, implemented in a small subset of the language, and a compiler for this small subset (in another language). Developing a reference interpreter is valuable independently of debootstrapping: it may help clarify the language semantics, and can be reused for other purposes such as differential testing of the other implementations. Grounding: We present Camlboot, our project to debootstrap the OCaml compiler, version 4.07. Once we converged on this final design, the last version of Camlboot took about a person-month of implementation effort, demonstrating feasibility. Using diverse double-compilation, we were able to prove the absence of trusting trust attack in the existing bootstrap of the standard OCaml implementation. Importance: To our knowledge, this document is the first scholarly discussion of "tailored" debootstrapping for high-level programming languages. Debootstrapping is an interesting problem which recently grew an active community of free software contributors, but so far the interactions with the programming-language research community have been minimal. We share our experience on Camlboot, trying to highlight aspects that are of interest to other language designers and implementors; we hope to foster stronger ties between the Bootstrappable project and relevant academic communities. In particular, the debootstrapping experience has been an interesting reflection on OCaml design and implementation, and we hope that other language implementors would find it equally valuable.

cs.PL↗

arXiv2021

Tail Modulo Cons

OCaml function calls consume space on the system stack. Operating systems set default limits on the stack space which are much lower than the available memory. If a program runs out of stack space, they get the dreaded "Stack Overflow" exception -- they crash. As a result, OCaml programmers have to be careful, when they write recursive functions, to remain in the so-called _tail-recursive_ fragment, using _tail_ calls that do not consume stack space. This discipline is a source of difficulties for both beginners and experts. Beginners have to be taught recursion, and then tail-recursion. Experts disagree on the "right" way to write `List.map`. The direct version is beautiful but not tail-recursive, so it crashes on larger inputs. The naive tail-recursive transformation is (slightly) slower than the direct version, and experts may want to avoid that cost. Some libraries propose horrible implementations, unrolling code by hand, to compensate for this performance loss. In general, tail-recursion requires the programmer to manually perform sophisticated program transformations. In this work we propose an implementation of "Tail Modulo Cons" (TMC) for OCaml. TMC is a program transformation for a fragment of non-tail-recursive functions, that rewrites them in _destination-passing style_. The supported fragment is smaller than other approaches such as continuation-passing-style, but the performance of the transformed code is on par with the direct, non-tail-recursive version. Many useful functions that traverse a recursive datastructure and rebuild another recursive structure are in the TMC fragment, in particular `List.map` (and `List.filter`, `List.append`, etc.). Finally those functions can be written in a way that is beautiful, correct on all inputs, and efficient.

cs.PL↗

arXiv2019

Dependent Pearl: Normalization by realizability

For those of us who generally live in the world of syntax, semantic proof techniques such as reducibility, realizability or logical relations seem somewhat magical despite -- or perhaps due to -- their seemingly unreasonable effectiveness. Why do they work? At which point in the proof is "the real work" done? Hoping to build a programming intuition of these proofs, we implement a normalization argument for the simply-typed lambda-calculus with sums: instead of a proof, it is described as a program in a dependently-typed meta-language. The semantic technique we set out to study is Krivine's classical realizability, which amounts to a proof-relevant presentation of reducibility arguments -- unary logical relations. Reducibility assigns a predicate to each type, realizability assigns a set of realizers, which are abstract machines that extend lambda-terms with a first-class notion of contexts. Normalization is a direct consequence of an adequacy theorem or "fundamental lemma", which states that any well-typed term translates to a realizer of its type. We show that the adequacy theorem, when written as a dependent program, corresponds to an evaluation procedure. In particular, a weak normalization proof precisely computes a series of reduction from the input term to a normal form. Interestingly, the choices that we make when we define the reducibility predicates -- truth and falsity witnesses for each connective -- determine the evaluation order of the proof, with each datatype constructor behaving in a lazy or strict fashion. While most of the ideas in this presentation are folklore among specialists, our dependently-typed functional program provides an accessible presentation to a wider audience. In particular, our work provides a gentle introduction to abstract machine calculi which have recently been used as an effective research vehicle.

cs.PL↗

arXiv2019

Functional programming with lambda-tree syntax

We present the design of a new functional programming language, MLTS, that uses the lambda-tree syntax approach to encoding bindings appearing within data structures. In this approach, bindings never become free nor escape their scope: instead, binders in data structures are permitted to move to binders within programs. The design of MLTS includes additional sites within programs that directly support this movement of bindings. In order to formally define the language's operational semantics, we present an abstract syntax for MLTS and a natural semantics for its evaluation. We shall view such natural semantics as a logical theory within a rich logic that includes both *nominal abstraction* and the *nabla-quantifier*: as a result, the natural semantics specification of MLTS can be given a succinct and elegant presentation. We present a typing discipline that naturally extends the typing of core ML programs and we illustrate the features of MLTS by presenting several examples. An on-line interpreter for MLTS is briefly described.

cs.PL↗

arXiv2019

Proceedings ML Family / OCaml Users and Developers workshops

This volume contains the joint post-proceedings of the 2017 editions of the ML Family Workshop and the OCaml Users and Developers Workshop which took place in Oxford, UK, September 2017, and which were colocated with the ICFP 2017 conference.

cs.PL↗

arXiv2018

A Practical Mode System for Recursive Definitions

In call-by-value languages, some mutually-recursive value definitions can be safely evaluated to build recursive functions or cyclic data structures, but some definitions (let rec x = x + 1) contain vicious circles and their evaluation fails at runtime. We propose a new static analysis to check the absence of such runtime failures. We present a set of declarative inference rules, prove its soundness with respect to the reference source-level semantics of Nordlander, Carlsson, and Gill (2008), and show that it can be (right-to-left) directed into an algorithmic check in a surprisingly simple way. Our implementation of this new check replaced the existing check used by the OCaml programming language, a fragile syntactic/grammatical criterion which let several subtle bugs slip through as the language kept evolving. We document some issues that arise when advanced features of a real-world functional language (exceptions in first-class modules, GADTs, etc.) interact with safety checking for recursive definitions.

cs.PL↗

arXiv2018

Unboxing Mutually Recursive Type Definitions in OCaml

In modern OCaml, single-argument datatype declarations (variants with a single constructor, records with a single field) can sometimes be `unboxed'. This means that their memory representation is the same as their single argument (omitting the variant or record constructor and an indirection), thus achieving better time and memory efficiency. However, in the case of generalized/guarded algebraic datatypes (GADTs), unboxing is not always possible due to a subtle assumption about the runtime representation of OCaml values. The current correctness check is incomplete, rejecting many valid definitions, in particular those involving mutually-recursive datatype declarations. In this paper, we explain the notion of separability as a semantic for the unboxing criterion, and propose a set of inference rules to check separability. From these inference rules, we derive a new implementation of the unboxing check that properly supports mutually-recursive definitions.

cs.PL↗

arXiv2018

Merlin: A Language Server for OCaml (Experience Report)

We report on the experience of developing Merlin, a language server for the OCaml programming language in development since 2013. Merlin is a daemon that connects to your favourite text editor and provides services that require a fine-grained understanding of the programming language syntax and static semantics: instant feedback on warnings and errors, autocompletion, `type of the code under the cursor', `go to definition', etc. Language servers need to handle incomplete and partially-incorrect programs, and try to be incremental to minimize recomputation after small editing actions. Merlin was built by carefully adapting the existing tools (the OCamllex lexer and Menhir parser generators) to better support incrementality, incompleteness and error handling. These extensions are elegant and general, as demonstrated by the interesting, unplanned uses that the OCaml community found for them. They could be adapted to other frontends -- in any language. Besides incrementality, we discuss the way Merlin communicates with editors, describe the design decisions that went into some demanding features and report on some of the non-apparent difficulties in building good editor support, emerging from expressive programming languages or frustrating tooling ecosystems. We expect this experience report to be of interest to authors of interactive language tooling for any programming language; many design choices may be reused, and some hard-won lessons can serve as warnings.

cs.PL↗

arXiv2017

Correctness of Speculative Optimizations with Dynamic Deoptimization

High-performance dynamic language implementations make heavy use of speculative optimizations to achieve speeds close to statically compiled languages. These optimizations are typically performed by a just-in-time compiler that generates code under a set of assumptions about the state of the program and its environment. In certain cases, a program may execute code compiled under assumptions that are no longer valid. The implementation must then deoptimize the program on-the-fly; this entails finding semantically equivalent code that does not rely on invalid assumptions, translating program state to that expected by the target code, and transferring control. This paper looks at the interaction between optimization and deoptimization, and shows that reasoning about speculation is surprisingly easy when assumptions are made explicit in the program representation. This insight is demonstrated on a compiler intermediate representation, named \sourir, modeled after the high-level representation for a dynamic language. Traditional compiler optimizations such constant folding, dead code elimination, and function inlining are shown to be correct in the presence of assumptions. Furthermore, the paper establishes the correctness of compiler transformations specific to deoptimization: namely unrestricted deoptimization, predicate hoisting, and assume composition.

cs.PL↗

arXiv2017

Capturing the Future by Replaying the Past

Delimited continuations are the mother of all monads! So goes the slogan inspired by Filinski's 1994 paper, which showed that delimited continuations can implement any monadic effect, letting the programmer use an effect as easily as if it was built into the language. It's a shame that not many languages have delimited continuations. Luckily, exceptions and state are also the mother of all monads! In this Pearl, we show how to implement delimited continuations in terms of exceptions and state, a construction we call $\textit{thermometer continuations}$. While traditional implementations of delimited continuations require some way of "capturing" an intermediate state of the computation, the insight of thermometer continuations is to reach this intermediate state by replaying the entire computation from the start, guiding it using a recording it so that the same thing happens until the captured point. Along the way, we explain delimited continuations and monadic reflection, show how the Filinski construction lets thermometer continuations express any monadic effect, share an elegant special-case for nondeterminism, and discuss why our construction is not prevented by theoretical results that exceptions and state cannot macro-express continuations.

cs.PL↗

arXiv2017

FabULous Interoperability for ML and a Linear Language

Instead of a monolithic programming language trying to cover all features of interest, some programming systems are designed by combining together simpler languages that cooperate to cover the same feature space. This can improve usability by making each part simpler than the whole, but there is a risk of abstraction leaks from one language to another that would break expectations of the users familiar with only one or some of the involved languages. We propose a formal specification for what it means for a given language in a multi-language system to be usable without leaks: it should embed into the multi-language in a fully abstract way, that is, its contextual equivalence should be unchanged in the larger system. To demonstrate our proposed design principle and formal specification criterion, we design a multi-language programming system that combines an ML-like statically typed functional language and another language with linear types and linear state. Our goal is to cover a good part of the expressiveness of languages that mix functional programming and linear state (ownership), at only a fraction of the complexity. We prove that the embedding of ML into the multi-language system is fully abstract: functional programmers should not fear abstraction leaks. We show examples of combined programs demonstrating in-place memory updates and safe resource handling, and an implementation extending OCaml with our linear language.

cs.PL↗

arXiv2016

Deciding equivalence with sums and the empty type

The logical technique of focusing can be applied to the $\lambda$-calculus; in a simple type system with atomic types and negative type formers (functions, products, the unit type), its normal forms coincide with $\beta\eta$-normal forms. Introducing a saturation phase gives a notion of quasi-normal forms in presence of positive types (sum types and the empty type). This rich structure let us prove the decidability of $\beta\eta$-equivalence in presence of the empty type, the fact that it coincides with contextual equivalence, and a finite model property.

cs.PL↗