SPLS online — June 30th

Most interaction with a computer is done via a graphical user interface. Traditionally, these are implemented in an imperative fashion using shared mutable state and callbacks. This is efficient, but is also difficult to reason about and error prone. Functional Reactive Programming (FRP) provides an elegant alternative which allows GUIs to be designed in a declarative fashion. However, most FRP languages are synchronous and continually check for new data. This means that an FRP-style GUI will “wake up” on each program cycle. This is problematic for applications like text editors and browsers, where often nothing happens for extended periods of time, and we want the implementation to sleep until new data arrives. In this paper, we present an asynchronous FRP language for designing GUIs called λWidget. Our language provides a novel semantics for widgets, the building block of GUIs, which offers both a natural Curry–Howard logical interpretation and an efficient implementation strategy.

Equality saturation is a rewrite-driven optimization technique which leverages a special data structure called e-graph to efficiently represent many variants of a rewritten expressions.

However, challenges arise when applying this technique to optimize functional programs. How can we for example efficiently implement alpha-equivalence; substitution for beta-reduction; or predicates for eta-reduction?

In this talk, we investigate different solutions to address these challenges, such as using De-Bruijn indices instead of named identifiers.

We show their impact in practice when optimizing programs expressed in Rise: a typed lambda calculus.

We will show that the presented solutions enable us to discover more complex optimizations than a naive implementation, although scaling the technique further remains an open challenge.

I'll outline what it would take to implement a "Nominal" package in an arbitrary programming language, generalising from my experience from designing the Nominal Haskell package.

We present handler calculus, a core calculus of effect handlers. Inspired by the Frank programming language, handler calculus does not have primitive functions, just handlers. Functions, products, sums, and inductive types, are all encodable in handler calculus. We extend handler calculus with recursive effects, which we use to encode recursive data types. We extend handler calculus with parametric operations, which we use to encode existential data types. We then briefly outline how one can encode universal data types by composing a CPS translation for parametric handler calculus into System F with Fujita’s CPS translation of System F into minimal existential logic.

Binary session types guarantee communication safety and session fidelity, but alone they cannot rule out deadlocks arising from the interleaving of different sessions.
In Classical Processes (CP)—a process calculus based on classical linear logic—deadlock freedom is guaranteed by combining channel creation and parallel composition under the same logical cut rule. Similarly, in Good Variation (GV)—a linear concurrent λ-calculus—deadlock freedom is guaranteed by combining channel creation and thread spawning under the same operation, called fork.
In both CP and GV, deadlock freedom is achieved at the expense of expressivity, as the only processes allowed are tree-structured. Dardha and Gay define Priority CP (PCP), which allows cyclic-structured processes and restores deadlock freedom by using priorities, in line with Kobayashi and Padovani.
Following PCP, we present Priority GV (PGV), a variant of GV which decouples channel creation from thread spawning. Consequently, we type cyclic-structured processes and restore deadlock freedom by using priorities. We show that our type system is sound by proving subject reduction and progress. We define an encoding from PCP to PGV and prove that the encoding preserves typing and is sound and complete with respect to the operational semantics.

Haskell’s performance can sometimes rival that of low-level languages. However, many of the performance-affecting decisions of the Glasgow Haskell Compiler (GHC) are informed by out-of-date heuristics typically evaluated on nofib, an out-of-date benchmark suite.

We investigated the case for upgrading GHC’s inliner by gathering performance data across real-world Haskell packages. To do so, we developed an updated benchmark suite and evaluated the impact of some of GHC's hard-coded constants, or "magic-numbers", on GHC’s inlining behaviour. Using these benchmarks, we demonstrated the potential for a 12.37 % geometric mean speedup.

This speedup is not attainable, however, without rewriting GHC’s inliner. With its current code, our analysis shows that a replacement of the inliner’s numerical thresholds—its magic numbers—would only yield a speedup of 5.36%, justifying a rethink of GHC’s inliner design.