Log in

No account? Create an account





July 29th, 2019


Typing, Representing, and Abstracting Control

Philipp Schuster and Jonathan Immanuel Brachthäuser, University of Tübingen, Germany

Abstract A well known technique to implement programming languages with delimited control operators shift and reset is to translate programs into continuation passing style (CPS). We can iterate the CPS translation to obtain the CPS hierarchy and to implement a family of control operators shifti and reseti. This functional pearl retells the story of a family of delimited control operators and their translation to lambda calculus via the CPS hierarchy. Prior work on the CPS hierarchy fixes a level of n-control operators for the entire program upfront, but we allow different parts of the program to live at different levels. It turns out that taking shift0 rather than shift as the basis for the family of control operators is essential for this. Our source language is a typed embedding in the dependently typed language Idris. Our target language is a HOAS embedding in Idris. The translation avoids administrative beta- and eta-redexes at all levels of the CPS hierarchy, by iterating well-known techniques for the non-iterated CPS translation

July 26th, 2019


An Operational Investigation of the CPS Hierarchy

Olivier Danvy (University of Aarhus, Denmark) and Zhe Yang (New York University, USA)

Abstract.We explore the hierarchy of control induced by successive transformations into continuation-passing style (CPS) in the presence of "control delimiters" and "composable continuations". Specifically, we investigate the structural operational semantics associated with the CPS hierarchy. To this end, we characterize an operational notion of continuation semantics. We relate it to the traditional CPS transformation and we use it to account for the control operator shift and the control delimiter reset operationally. We then transcribe the resulting continuation semantics in ML, thus obtaining a native and modular implementation of the entire hierarchy. We illustrate it with several examples, the most significant of which is layered monads.

Typing Control Operators in the CPS Hierarchy

Małgorzata Biernacka University of Wrocław
Dariusz Biernacki University of Wrocław
Sergueı Lenglet University of Wrocław

Abstract. The CPS hierarchy of Danvy and Filinski is a hierarchy of continuations that allows for expressing nested control effects characteristic of, e.g., non-deterministic programming or certain instances of normalization by evaluation. In this article, we present a comprehensive study of a typed version of the CPS hierarchy, where the typing discipline generalizes Danvy and Filinski’s type system for control operators shift and reset. To this end, we define a typed family of control operators that give access to delimited continuations in the CPS hierarchy and that are slightly more flexible than Danvy and Filinski’s family of control operators shifti and reseti, but, as we show, are equally expressive. For this type system, we prove subject reduction, soundness with respect to the CPS translation, and termination of evaluation. We also show that our results scale to a type system for even more flexible control operators expressible in the CPS hierarchy.

A Substructural Type System for Delimited Continuations

Oleg Kiselyov and Chung-chieh Shan

Abstract. We propose type systems that abstractly interpret small-step rather than big-step operational semantics. We treat an expression or evaluation context as a structure in a linear logic with hypothetical reasoning. Evaluation order is not only regulated by familiar focusing rules in the operational semantics, but also expressed by structural rules in the type system, so the types track control flow more closely. Binding and evaluation contexts are related, but the latter are linear. We use these ideas to build a type system for delimited continuations. It lets control operators change the answer type or act beyond the nearest dynamically-enclosing delimiter, yet needs no extra fields in judgments and arrow types to record answer types. The typing derivation of a direct-style program desugars it into continuation-passing style.

A Dynamic Interpretation of the CPS Hierarchy

Marek Materzok and Dariusz Biernacki, University of Wrocław, Wrocław, Poland

Abstract: The CPS hierarchy of control operators shifti / reseti of Danvy and Filinski is a natural generalization of the shift and reset static control operators that allow for abstracting delimited control in a structured and CPS-guided manner. In this article we show that a dynamic variant of shift/reset, known as shift0 / reset0, where the discipline of static access to the stack of delimited continuations is relaxed, can fully express the CPS hierarchy. This result demonstrates the expressive power of shift0 / reset0 and it offers a new perspective on practical applications of the CPS hierarchy.

July 21st, 2019


Most of the existing literature about monadic programming focuses on theory but does not address issues of software engineering. Using monadic parsing as a running example, we demonstrate monadic programs written in a typical style, recognize how they violate abstraction boundaries, and recover clean abstraction crossings through monadic reflection. Once monadic reflection is made explicit, it is possible to construct a grammar for monadic programming that is independent of domain-specific operations. This grammar, in turn, enables the redefinition of the monadic operators as macros that eliminate at expansion time the overhead imposed by functional representations. The results are very efficient monadic programs; for parsing, the output code is competitive with good hand-crafted parsers.

July 9th, 2019


Toru Kawata
Department of Computer Science, The University of Tokyo, Tokyo, Japan kawata@lyon.is.s.u-tokyo.ac.jp

With the help of an idea of contextual modal logic, we define a logical system λrefl that in-
corporates monadic reflection, and then investigate delimited continuations through the lens of monadic reflection. Technically, we firstly prove a certain universality of continuation monad, making the character of monadic reflection a little more clear. Next, moving focus to delimited continuations, we present a macro definition of shift/reset by monadic reflection. We then prove that λrefl , a restriction of λrefl, has exactly the same provability as λs/r , a system that incorpo- 2cont pure rates shift/reset. Our reconstruction of monadic reflection opens up a path for investigation of delimited continuations with familiar monadic language.
Powered by LiveJournal.com