Effect handlers have recently gained popularity amongst programming language researchers. Existing type- and effect systems for effect handlers are often complicated and potentially hinder a ...wide-spread adoption. We present the language Effekt with the goal to close the gap between research languages with effect handlers and languages for working programmers. The design of Effekt revolves around a different view of effects and effect types. Traditionally, effect types express which side effects a computation might have. In Effekt, effect types express which capabilities a computation requires from its context. While this new point in the design space of effect systems impedes reasoning about purity, we demonstrate that it simplifies the treatment of effect polymorphism and the related issues of effect parametricity and effect encapsulation. To guarantee effect safety, we separate functions from values and treat all functions as second-class. We define the semantics of Effekt as a translation to System Xi, a calculus in explicit capability-passing style.
Compiling effect handlers in capability-passing style Schuster, Philipp; Brachthäuser, Jonathan Immanuel; Ostermann, Klaus
Proceedings of ACM on programming languages,
08/2020, Letnik:
4, Številka:
ICFP
Journal Article
Recenzirano
Odprti dostop
Effect handlers encourage programmers to abstract over repeated patterns of complex control flow. As of today, this abstraction comes at a significant price in performance. In this paper, we aim to ...achieve abstraction without regret for effect handlers.
We present a language for effect handlers in _capability-passing style_ (λ
Cap
) and an implementation of this language as a translation to simply-typed lambda calculus in _iterated continuation-passing style_. A suite of benchmarks indicates that the novel combination of capability-passing style and iterated CPS enables significant speedups over existing languages with effect handlers or control operators. Our implementation technique is general and allows us to generate code in any language that supports first-class functions.
We then identify a subset of programs for which we can further improve the performance and guarantee full elimination of the effect handler abstraction. To formally capture this subset, we refine λ
Cap
to λ λ
Cap
with a more restrictive type system. We present a type-directed translation for λ λ
Cap
that inserts staging annotations and prove that no abstractions or applications related to effect handlers occur in the translated program. Using this second translation we observe additional speedups in some of the benchmarks.
We present a modular semantic account of Bayesian inference algorithms for probabilistic programming languages, as used in data science and machine learning. Sophisticated inference algorithms are ...often explained in terms of composition of smaller parts. However, neither their theoretical justification nor their implementation reflects this modularity. We show how to conceptualise and analyse such inference algorithms as manipulating intermediate representations of probabilistic programs using higher-order functions and inductive types, and their denotational semantics.
Semantic accounts of continuous distributions use measurable spaces. However, our use of higher-order functions presents a substantial technical difficulty: it is impossible to define a measurable space structure over the collection of measurable functions between arbitrary measurable spaces that is compatible with standard operations on those functions, such as function application. We overcome this difficulty using quasi-Borel spaces, a recently proposed mathematical structure that supports both function spaces and continuous distributions.
We define a class of semantic structures for representing probabilistic programs, and semantic validity criteria for transformations of these representations in terms of distribution preservation. We develop a collection of building blocks for composing representations. We use these building blocks to validate common inference algorithms such as Sequential Monte Carlo and Markov Chain Monte Carlo. To emphasize the connection between the semantic manipulation and its traditional measure theoretic origins, we use Kock's synthetic measure theory. We demonstrate its usefulness by proving a quasi-Borel counterpart to the Metropolis-Hastings-Green theorem.
Effect handlers for the masses Brachthäuser, Jonathan Immanuel; Schuster, Philipp; Ostermann, Klaus
Proceedings of ACM on programming languages,
11/2018, Letnik:
2, Številka:
OOPSLA
Journal Article
Recenzirano
Odprti dostop
Effect handlers are a program structuring paradigm with rising popularity in the functional programming language community and can express many advanced control flow abstractions. We present the ...first implementation of effect handlers for Java - an imperative, object oriented programming language. Our framework consists of three core components: A type selective CPS transformation via JVM bytecode transformation, an implementation of delimited continuations on top of the bytecode transformation and finally a library for effect handlers in terms of delimited continuations.
Software product line engineering is an efficient means to generate a set of tailored software products from a common implementation. However, adopting a product-line approach poses a major challenge ...and significant risks, since typically legacy code must be migrated toward a product line. Our aim is to lower the adoption barrier by providing semi-automatic tool support-called variability mining -to support developers in locating, documenting, and extracting implementations of product-line features from legacy code. Variability mining combines prior work on concern location, reverse engineering, and variability-aware type systems, but is tailored specifically for the use in product lines. Our work pursues three technical goals: (1) we provide a consistency indicator based on a variability-aware type system, (2) we mine features at a fine level of granularity, and (3) we exploit domain knowledge about the relationship between features when available. With a quantitative study, we demonstrate that variability mining can efficiently support developers in locating features.
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 library implementation of effect handlers that supports effect safety and effect polymorphism without resorting to type-level programming. We describe a novel way of achieving effect safety using intersection types and path-dependent types. The effect system of our library design fits well into the programming paradigm of capability passing and is inspired by the effect system of Zhang & Myers (2019,
Proc. ACM Program. Lang.
3
(POPL), 5:1-5:29). Capabilities carry an abstract type member, which represents an individual effect type and reflects the use of the capability on the type level. We represent effect rows as the contravariant intersection of effect types. Handlers introduce capabilities and remove components of the intersection type. Reusing the existing type system of Scala, we get effect subtyping and effect polymorphism for free.
The expression problem describes how most types can easily be extended with new ways to produce the type or new ways to consume the type, but not both. When abstract syntax trees are defined as an ...algebraic data type, for example, they can easily be extended with new consumers, such as print or eval, but adding a new constructor requires the modification of all existing pattern matches. The expression problem is one way to elucidate the difference between functional or data-oriented programs (easily extendable by new consumers) and object-oriented programs (easily extendable by new producers). This difference between programs which are extensible by new producers or new consumers also exists for dependently typed programming, but with one core difference: Dependently-typed programming almost exclusively follows the functional programming model and not the object-oriented model, which leaves an interesting space in the programming language landscape unexplored. In this paper, we explore the field of dependently-typed object-oriented programming by deriving it from first principles using the principle of duality. That is, we do not extend an existing object-oriented formalism with dependent types in an ad-hoc fashion, but instead start from a familiar data-oriented language and derive its dual fragment by the systematic use of defunctionalization and refunctionalization. Our central contribution is a dependently typed calculus which contains two dual language fragments. We provide type- and semantics-preserving transformations between these two language fragments: defunctionalization and refunctionalization. We have implemented this language and these transformations and use this implementation to explain the various ways in which constructions in dependently typed programming can be explained as special instances of the general phenomenon of duality.
Back to Direct Style: Typed and Tight Müller, Marius; Schuster, Philipp; Brachthäuser, Jonathan Immanuel ...
Proceedings of ACM on programming languages,
04/2023, Letnik:
7, Številka:
OOPSLA1
Journal Article
Recenzirano
Odprti dostop
Translating programs into continuation-passing style is a well-studied tool to explicitly deal with the control structure of programs. This is useful, for example, for compilation. In a typed ...setting, there also is a logical interpretation of such a translation as an embedding of classical logic into intuitionistic logic. A naturally arising question is whether there is an inverse translation back to direct style. The answer to this question depends on how the continuation-passing translation is defined and on the domain of the inverse translation. In general, translating programs from continuation-passing style back to direct style requires the use of control operators to account for the use of continuations in non-trivial ways. We present two languages, one in direct style and one in continuation-passing style. Both languages are typed and equipped with an abstract machine semantics. Moreover, both languages allow for non-trivial control flow. We further present a translation to continuation-passing style and a translation back to direct style. We show that both translations are type-preserving and also preserve semantics in a very precise way giving an operational correspondence between the two languages. Moreover, we show that the compositions of the translations are well-behaved. In particular, they are syntactic one-sided inverses on the full language and full syntactic inverses when restricted to trivial control flow.
The expression problem describes a fundamental trade-off in program design: Should a program's primary decomposition be determined by the way its domain objects are constructed ("functional" ...decomposition), or by the way they are destructed ("object-oriented" decomposition)? We argue that programming languages should not force one of these decompositions on the programmer; rather, a programming language should support both ways of decomposing a program in a symmetric way, with an easy translation between these decompositions. However, current programming languages are usually not symmetric and hence make it unnecessarily hard to switch the decomposition.
We propose a language that is symmetric in this regard and allows a fully automatic translation between "functional" and "object-oriented" decomposition. We present a language with algebraic data types and pattern matching for "functional" decomposition and codata types and copattern matching for "object-oriented" decomposition, together with a bijective translation that turns a data type into a codata type ("destructorization") or vice versa ("constructorization"). We present the first symmetric programming language with support for local (co)pattern matching, which includes local anonymous function or object definitions, that allows an automatic translation as described above. We also present the first mechanical formalization of such a language and prove i) that the type system is sound, that the translations between data and codata types are ii) type-preserving, iii) behavior-preserving and iv) inverses of each other. We also extract a mechanically verified implementation from our formalization and have implemented an IDE with direct support for these translations.
Introduction and elimination, left and right Ostermann, Klaus; Binder, David; Skupin, Ingo ...
Proceedings of ACM on programming languages,
08/2022, Letnik:
6, Številka:
ICFP
Journal Article
Recenzirano
Odprti dostop
Functional programming language design has been shaped by the framework of natural deduction, in which language constructs are divided into introduction and elimination rules for
producers
of values. ...In sequent calculus-based languages, left introduction rules replace (right) elimination rules and provide a dedicated sublanguage for
consumers
of values. In this paper, we present and analyze a wider design space of programming languages which encompasses four kinds of rules: Introduction and elimination, both left and right. We analyze the influence of rule choice on program structure and argue that having all kinds of rules enriches a programmer’s modularity arsenal. In particular, we identify four ways of adhering to the principle that ”the structure of the program follows the structure of the data“ and show that they correspond to the four possible choices of rules. We also propose the principle of
bi-expressibility
to guide and validate the design of rules for a connective. Finally, we deepen the well-known dualities between different connectives by means of the proof/refutation duality.
PDF
