arXiv subjects

Sam Lindley

Publications and source records attributed to Sam Lindley.

At least 19 recordsLinked to original sources

arXiv2026

Finitary Semantics for Full Ground Local State

Full ground local state (FGLS) refers to dynamically allocated mutable state that allows storing ground values and references. It is a key ingredient in many imperative algorithms as it enables (cyclic) data structures. In this work, we treat full ground local state as a computational effect, focusing on one particular denotational model: Kammar et al.'s possible worlds monad on sets indexed over sets of locations. We resolve an outstanding question regarding this FGLS monad: is it finitary? We show that the FGLS monad is not finitary by showing the existence of non-finitary computations in the monad. We then introduce a finitary submonad of Kammar et al.'s monad, give it a concrete description and show that it provides an adequate semantics for FGLS. The submonad we construct paves the way to understanding FGLS in the future via an equational axiomatization suitable for program reasoning.

cs.PL↗

arXiv2026

Bidirectional Typing with Freezing, Skeletons, and Ghosts

Bidirectional typing makes use of local information flow between functions and arguments. Conventional bidirectional typing only supports unidirectional information flow, typically from functions to arguments, which is insufficient to infer first-class polymorphism. Existing work on improving information flow either has limited support for mixed information flow or requires ad hoc mechanisms that harm predictability. We propose Fresco, a novel bidirectional type inference approach to first-class polymorphism. Fresco enables local type information to flow back and forth between functions and arguments via skeletons, with ghosts representing unknown type information, and allows users to customise the direction of information flow by freezing. The flexible information flow of Fresco enables expressive and predictable inference for first-class polymorphism. We provide a declarative specification for Fresco, a simple type inference algorithm that is sound and complete with respect to the declarative system, and a prototype implementation that further generalises Fresco to infer modal effect types.

cs.PL↗

arXiv2026

An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories

We use the theory of algebraic effects to give a complete equational axiomatization for dynamic threads. Our method is based on parameterized algebraic theories, which give a concrete syntax for strong monads on functor categories, and are a convenient framework for names and binding. Our programs are built from the key primitives `fork' and `wait'. `Fork' creates a child thread and passes its name (thread ID) to the parent thread. `Wait' allows us to wait for given child threads to finish. We provide a parameterized algebraic theory built from fork and wait, together with basic atomic actions and laws such as associativity of `fork'. Our equational axiomatization is complete in two senses. First, for closed expressions, it completely captures equality of labelled posets (pomsets), an established model of concurrency: model complete. Second, any two open expressions are provably equal if they are equal under all closing substitutions: syntactically complete. The benefit of algebraic effects is that the semantic analysis can focus on the algebraic operations of fork and wait. We then extend the analysis to a simple concurrent programming language by giving operational and denotational semantics. The denotational semantics is built using the methods of parameterized algebraic theories and we show that it is sound, adequate, and fully abstract at first order for labelled-poset observations.

cs.PL↗

arXiv2025

Rows and Capabilities as Modal Effects

Effect handlers allow programmers to model and compose computational effects modularly. Effect systems statically guarantee that all effects are handled. Several recent practical effect systems are based on either row polymorphism or capabilities. However, there remains a gap in understanding the precise relationship between effect systems with such disparate foundations. The main difficulty is that in both row-based and capability-based systems, effect tracking is typically entangled with other features such as functions. We propose a uniform framework for encoding, analysing, and comparing effect systems. Our framework exploits and generalises modal effect types, a recent novel effect system which decouples effect tracking from functions via modalities. Modalities offer fine-grained control over when and how effects are tracked, enabling us to express different strategies for effect tracking. We give encodings as macro translations from existing row-based and capability-based effect systems into our framework and show that these encodings preserve types and semantics. Our encodings reveal the essence of effect tracking mechanisms in different effect systems, enable a direct analysis on their differences, and provide practical insights on language design.

cs.PL↗

arXiv2024

Modal Effect Types

Effect handlers are a powerful abstraction for defining, customising, and composing computational effects. Statically ensuring that all effect operations are handled requires some form of effect system, but using a traditional effect system would require adding extensive effect annotations to the millions of lines of existing code in these languages. Recent proposals seek to address this problem by removing the need for explicit effect polymorphism. However, they typically rely on fragile syntactic mechanisms or on introducing a separate notion of second-class function. We introduce a novel approach based on modal effect types.

cs.PL↗

arXiv2024

Behavioural Types for Heterogeneous Systems (Position Paper)

Behavioural types provide a promising way to achieve lightweight, language-integrated verification for communication-centric software. However, a large barrier to the adoption of behavioural types is that the current state of the art expects software to be written using the same tools and typing discipline throughout a system, and has little support for components over which a developer has no control. This position paper describes the outcomes of a working group discussion at Dagstuhl Seminar 24051 (Next-Generation Protocols for Heterogeneous Systems). We propose a methodology for integrating multiple behaviourally-typed components, written in different languages. Our proposed approach involves an extensible protocol description language, a session IR that can describe data transformations and boundary monitoring and which can be compiled into program-specific session proxies, and finally a session middleware to aid session establishment. We hope that this position paper will stimulate discussion on one of the most pressing challenges facing the widespread adoption of behavioural typing.

cs.PL↗

arXiv2024

Scoped Effects as Parameterized Algebraic Theories

Notions of computation can be modelled by monads. Algebraic effects offer a characterization of monads in terms of algebraic operations and equational axioms, where operations are basic programming features, such as reading or updating the state, and axioms specify observably equivalent expressions. However, many useful programming features depend on additional mechanisms such as delimited scopes or dynamically allocated resources. Such mechanisms can be supported via extensions to algebraic effects including scoped effects and parameterized algebraic theories. We present a fresh perspective on scoped effects by translation into a variation of parameterized algebraic theories. The translation enables a new approach to equational reasoning for scoped effects and gives rise to an alternative characterization of monads in terms of generators and equations involving both scoped and algebraic operations. We demonstrate the power of our fresh perspective by way of equational characterizations of several known models of scoped effects.

cs.PL↗

arXiv2023

Wasm SpecTec: Engineering a Formal Language Standard

WebAssembly (Wasm) is a low-level bytecode language and virtual machine, intended as a compilation target for a wide range of programming languages, which is seeing increasing adoption across diverse ecosystems. As a young technology, Wasm continues to evolve -- it reached version 2.0 last year and another major update is expected soon. For a new feature to be standardised in Wasm, four key artefacts must be presented: a formal (mathematical) specification of the feature, an accompanying prose pseudocode description, an implementation in the official reference interpreter, and a suite of unit tests. This rigorous process helps to avoid errors in the design and implementation of new Wasm features, and Wasm's distinctive formal specification in particular has facilitated machine-checked proofs of various correctness properties for the language. However, manually crafting all of these artefacts requires expert knowledge combined with repetitive and tedious labor, which is a burden on the language's standardization process and authoring of the specification. This paper presents Wasm SpecTec, a technology to express the formal specification of Wasm through a domain-specific language. This DSL allows all of Wasm's currently handwritten specification artefacts to be error-checked and generated automatically from a single source of truth, and is designed to be easy to write, read, compare, and review. We believe that Wasm SpecTec's automation and meta-level error checking will significantly ease the current burden of the language's specification authors. We demonstrate the current capabilities of Wasm SpecTec by showcasing its proficiency in generating various artefacts, and describe our work towards replacing the manually written official Wasm specification document with specifications generated by Wasm SpecTec.

cs.PL↗

arXiv2023

Continuing WebAssembly with Effect Handlers

WebAssembly (Wasm) is a low-level portable code format offering near native performance. It is intended as a compilation target for a wide variety of source languages. However, Wasm provides no direct support for non-local control flow features such as async/await, generators/iterators, lightweight threads, first-class continuations, etc. This means that compilers for source languages with such features must ceremoniously transform whole source programs in order to target Wasm. We present WasmFX, an extension to Wasm which provides a universal target for non-local control features via effect handlers, enabling compilers to translate such features directly into Wasm. Our extension is minimal and only adds three main instructions for creating, suspending, and resuming continuations. Moreover, our primitive instructions are type-safe providing typed continuations which are well-aligned with the design principles of Wasm whose stacks are typed. We present a formal specification of WasmFX and show that the extension is sound. We have implemented WasmFX as an extension to the Wasm reference interpreter and also built a prototype WasmFX extension for Wasmtime, a production-grade Wasm engine, piggybacking on Wasmtime's existing fibers API. The preliminary performance results for our prototype are encouraging, and we outline future plans to realise a native implementation

cs.PL↗

arXiv2023

Soundly Handling Linearity

We propose a novel approach to soundly combining linear types with effect handlers. Linear type systems statically ensure that resources such as file handles are used exactly once. Effect handlers provide a modular programming abstraction for implementing features ranging from exceptions to concurrency. Whereas linear type systems bake in the assumption that continuations are invoked exactly once, effect handlers allow continuations to be discarded or invoked more than once. This mismatch leads to soundness bugs in existing systems such as the programming language Links, which combines linearity (for session types) with effect handlers. We introduce control flow linearity as a means to ensure that continuations are used in accordance with the linearity of any resources they capture, ruling out such soundness bugs. We formalise control flow linearity in a System F-style core calculus Feffpop equipped with linear types, effect types, and effect handlers. We define a linearity-aware semantics to formally prove that Feffpop preserves the integrity of linear values in the sense that no linear value is discarded or duplicated. In order to show that control flow linearity can be made practical, we adapt Links based on the design of Feffpop, in doing so fixing a long-standing soundness bug. Finally, to better expose the potential of control flow linearity, we define an ML-style core calculus Qeffpop, based on qualified types, which requires no programmer provided annotations, and instead relies entirely on type inference to infer control flow linearity. Both linearity and effects are captured by qualified types. Qeffpop overcomes a number of practical limitations of Feffpop, supporting abstraction over linearity, linearity dependencies between type variables, and a much more fine-grained notion of control flow linearity.

cs.PL↗

arXiv2023

Structural Subtyping as Parametric Polymorphism

Structural subtyping and parametric polymorphism provide similar flexibility and reusability to programmers. For example, both features enable the programmer to provide a wider record as an argument to a function that expects a narrower one. However, the means by which they do so differs substantially, and the precise details of the relationship between them exists, at best, as folklore in literature. In this paper, we systematically study the relative expressive power of structural subtyping and parametric polymorphism. We focus our investigation on establishing the extent to which parametric polymorphism, in the form of row and presence polymorphism, can encode structural subtyping for variant and record types. We base our study on various Church-style $\lambda$-calculi extended with records and variants, different forms of structural subtyping, and row and presence polymorphism. We characterise expressiveness by exhibiting compositional translations between calculi. For each translation we prove a type preservation and operational correspondence result. We also prove a number of non-existence results. By imposing restrictions on both source and target types, we reveal further subtleties in the expressiveness landscape, the restrictions enabling otherwise impossible translations to be defined. More specifically, we prove that full subtyping cannot be encoded via polymorphism, but we show that several restricted forms of subtyping can be encoded via particular forms of polymorphism.

cs.PL↗

arXiv2022

Constraint-based type inference for FreezeML

FreezeML is a new approach to first-class polymorphic type inference that employs term annotations to control when and how polymorphic types are instantiated and generalised. It conservatively extends Hindley-Milner type inference and was first presented as an extension to Algorithm W. More modern type inference techniques such as HM(X) and OutsideIn($X$) employ constraints to support features such as type classes, type families, rows, and other extensions. We take the first step towards modernising FreezeML by presenting a constraint-based type inference algorithm. We introduce a new constraint language, inspired by the Pottier/R\'emy presentation of HM(X), in order to allow FreezeML type inference problems to be expressed as constraints. We present a deterministic stack machine for solving FreezeML constraints and prove its termination and correctness.

cs.PL↗

arXiv2021

A Typed Slicing Compilation of the Polymorphic RPC Calculus

The polymorphic RPC calculus allows programmers to write succinct multitier programs using polymorphic location constructs. However, until now it lacked an implementation. We develop an experimental programming language based on the polymorphic RPC calculus. We introduce a polymorphic Client-Server (CS) calculus with the client and server parts separated. In contrast to existing untyped CS calculi, our calculus is not only able to resolve polymorphic locations statically, but it is also able to do so dynamically. We design a type-based slicing compilation of the polymorphic RPC calculus into this CS calculus, proving type and semantic correctness. We propose a method to erase types unnecessary for execution but retaining locations at runtime by translating the polymorphic CS calculus into an untyped CS calculus, proving semantic correctness.

cs.PL↗

arXiv2021

Separating Sessions Smoothly

This paper introduces Hypersequent GV (HGV), a modular and extensible core calculus for functional programming with session types that enjoys deadlock freedom, confluence, and strong normalisation. HGV exploits hyper-environments, which are collections of type environments, to ensure that structural congruence is type preserving. As a consequence we obtain an operational correspondence between HGV and HCP -- a process calculus based on hypersequents and in a propositions-as-types correspondence with classical linear logic (CLL). Our translations from HGV to HCP and vice-versa both preserve and reflect reduction. HGV scales smoothly to support Girard's Mix rule, a crucial ingredient for channel forwarding and exceptions.

cs.PL↗

arXiv2020

Effects for Efficiency: Asymptotic Speedup with First-Class Control

We study the fundamental efficiency of delimited control. Specifically, we show that effect handlers enable an asymptotic improvement in runtime complexity for a certain class of functions. We consider the generic count problem using a pure PCF-like base language $\lambda_b$ and its extension with effect handlers $\lambda_h$. We show that $\lambda_h$ admits an asymptotically more efficient implementation of generic count than any $\lambda_b$ implementation. We also show that this efficiency gap remains when $\lambda_b$ is extended with mutable state. To our knowledge this result is the first of its kind for control operators.

cs.PL↗

arXiv2020

Proceedings Eighth Workshop on Mathematically Structured Functional Programming

This volume contains the proceedings of the Eighth Workshop on Mathematically Structured Functional Programming (MSFP 2020). The meeting was originally scheduled to take place in Dublin, Ireland on the 25th of April as a satellite event of the European Joint Conferences on Theory & Practice of Software (ETAPS 2020). Due to the COVID-19 pandemic, ETAPS 2020, and consequently MSFP 2020, has been postponed to a date yet to be determined. The MSFP workshop highlights applications of mathematical structures to programming applications. We promote the use of category theory, type theory, and formal language semantics to the development of simple and reasonable programs. This year's papers cover a variety of topics ranging from array programming to dependent types to effects.

cs.PL↗

arXiv2020

FreezeML: Complete and Easy Type Inference for First-Class Polymorphism

ML is remarkable in providing statically typed polymorphism without the programmer ever having to write any type annotations. The cost of this parsimony is that the programmer is limited to a form of polymorphism in which quantifiers can occur only at the outermost level of a type and type variables can be instantiated only with monomorphic types. Type inference for unrestricted System F-style polymorphism is undecidable in general. Nevertheless, the literature abounds with a range of proposals to bridge the gap between ML and System F. We put forth a new proposal, FreezeML, a conservative extension of ML with two new features. First, let- and lambda-binders may be annotated with arbitrary System F types. Second, variable occurrences may be frozen, explicitly disabling instantiation. FreezeML is equipped with type-preserving translations back and forth between System F and admits a type inference algorithm, an extension of algorithm W, that is sound and complete and which yields principal types.

cs.PL↗

arXiv2019

A Polymorphic RPC Calculus

The RPC calculus is a simple semantic foundation for multi-tier programming languages such as Links in which located functions can be written for the client-server model. Subsequently, the typed RPC calculus is designed to capture the location information of functions by types and to drive location type-directed slicing compilations. However, the use of locations is currently limited to monomorphic ones, which is one of the gaps to overcome to put into practice the theory of RPC calculi for client-server model. This paper proposes a polymorphic RPC calculus to allow programmers to write succinct multi-tier programs using polymorphic location constructs. Then the polymorphic multi-tier programs can be automatically translated into programs only containing location constants amenable to the existing slicing compilation methods. We formulate a type system for the polymorphic RPC calculus, and prove its type soundness. Also, we design a monomorphization translation together with proofs on its type and semantic correctness for the translation.

cs.PL↗