Log in

No account? Create an account





Skipped Back 10

July 26th, 2019


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.

July 1st, 2019

Handlers in Action

Effect Handlers, Monadic Reflection, Delimited Control



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 practical implementation of effect handlers that supports effect safety, effect polymorphism, effect parametricity, and effect encapsulation which means that all effects are handled and effects cannot be accidentally handled by the wrong handler. Other existing languages and libraries break effect encapsulation by leaking implementation details in the effect type unless the user manually adds lifting annotations. We describe a novel way of achieving effect-safety using intersection types and path dependent types. We represent effect rows as the contravariant intersection of effect types, where an individual effect is represented by the singleton type of its capability. Handlers remove components of the intersection type. By reusing the existing type system we get subtyping and polymorphism of effects for free. The effect system not only guarantees safety, but also guarantees modular reasoning about higher-order effectful programs.

June 9th, 2019


Языки программирования от Фортрана и Кобола до Caml и Java играют ключевую роль в управлении сложными компьютерными системами. Книга «Введение в теорию языков программирования» представляет читателю средства, необходимые для проектирования и реализации подобных языков. В ней предлагается единый подход к различным формализмам для определения языков программирования – операционной и денотационной семантике. Особое внимание при этом уделяется способам задания отношений между тремя объектами: программой, входным значением и результатом. Эти формализмы демонстрируются на примере таких типичных элементов языков программирования, как функции, рекурсия, присваивание, записи и объекты. При этом показывается, что теория языков программирования состоит не в последовательном изучении самих языков один за другим, а строится вокруг механизмов, входящих в различные языки. Изучение таких механизмов в книге приводит к разработке вычислителей, интерпретаторов и компиляторов, а также к реализации алгоритмов вывода типов для учебных языков.
Powered by LiveJournal.com