916 papers · page 7 of 46
The Garsia–Wachs algorithm is an algorithm for building a binary leaf tree whose cost is as small as possible. The problem and the algorithm are described in more detail below, but the task is essentially the same as that of building a Huffman coding tree with the added constrain…
Abstract Effect handlers are a promising way to structure effectful programs in a modular way. We present the Scala library Effekt , which is centered around capability passing and implemented in terms of a monad for multi-prompt delimited continuations. Effekt is the first libra…
Abstract Actors collaborate via message exchanges to reach a common goal. Experience has shown, however, that pure message-based communication is limiting and forces developers to use design patterns. The recently introduced dataspace actor model borrows ideas from the tuple spac…
Abstract In a dependently typed language, we can guarantee correctness of our programmes by providing formal proofs. To check them, the typechecker elaborates these programs and proofs into a low-level core language. However, this core language is by nature hard to understand by …
Abstract We explore the design and implementation of Frank, a strict functional programming language with a bidirectional effect type system designed from the ground up around a novel variant of Plotkin and Pretnar’s effect handler abstraction. Effect handlers provide an abstract…
Abstract In ML-style module type theory, sealing often leads to situations in which type variables must leave scope, and this creates a need for signatures that avoid such variables. Unfortunately, in general, there is no best signature that avoids a variable, so modules do not a…
Algorithms in their purely functional form. Books on algorithms are plenty. Many present classical algorithms as entities carved in stone, conceived decades ago, and typeset in framed pseudo-code boxes. Not so in the present book. Bird and Gibbons treat any algorithm as a subject…
Abstract Plotkin and Pretnar’s effect handlers offer a versatile abstraction for modular programming with user-defined effects. This paper focuses on foundations for implementing effect handlers, for the three different kinds of effect handlers that have been proposed in the lite…
Many students complete PhDs in functional programming each year. As a service to the community, twice per year the Journal of Functional Programming publishes the abstracts from PhD dissertations completed during the previous year.
Many students complete PhDs in functional programming each year. As a service to the community, twice per year the Journal of Functional Programming publishes the abstracts from PhD dissertations completed during the previous year.
Abstract As popularity of algebraic effects and handlers increases, so does a demand for their efficient execution. Eff, an ML-like language with native support for handlers, has a subtyping-based effect system on which an effect-aware optimising compiler could be built. Unfortun…
Abstract From the outset, lambda calculus represented natural numbers through iterated application. The successor hence adds one more application, and the predecessor removes. In effect, the predecessor un-applies a term—which seemed impossible, even to Church. It took Kleene a r…
Abstract Algebraic effects are computational effects that can be described with a set of basic operations and equations between them. As many interesting effect handlers do not respect these equations, most approaches assume a trivial theory, sacrificing both reasoning power and …
Abstract Sheet-defined functions (SDFs) bring modularity and abstraction to the world of spreadsheets. Alas, end users naturally write SDFs that work over fixed-size arrays, which limits their reusability. To help end user programmers write more reusable SDFs, we describe a princ…
Abstract Build systems are awesome, terrifying – and unloved. They are used by every developer around the world, but are rarely the object of study. In this paper, we offer a systematic, and executable, framework for developing and comparing build systems, viewing them as related…
Type-Driven Development with IdrisProgramming languages that support dependent types provide us with an expressive environment in which we can specify and reason about properties of our software programs.Type-Driven Development with Idris is an introductory text to dependently ty…
Abstract Highly critical application domains, like medicine and aerospace, require the use of strict design, implementation, and validation techniques. Functional languages have been used in these domains to develop synchronous dataflow programming languages for reactive systems.…
Abstract Many types of interactive applications, including reactive systems implemented in hardware, interactive physics simulations and games, raise particular challenges when it comes to testing and debugging. Reasons include de facto lack of reproducibility and difficulties of…
Abstract Algebraic effects and handlers are a convenient method for structuring monadic effects with primitive effectful operations and separating the syntax from the interpretation of these operations. However, the scope of conventional handlers is limited as not all side effect…