Log in

No account? Create an account





September 15th, 2019




The call-by-need lambda calculus provides an equational framework for reasoning syntactically about lazy evaluation. This paper examines its operational characteristics. By a series of reasoning steps, we systematically unpack the standard-order reduction relation of the calculus and discover a novel abstract machine definition which, like the calculus, goes “under lambdas.” We prove that machine evaluation is equivalent to standard-order evaluation.Unlike traditional abstract machines, delimited control plays a significant role in the machine’s behavior. In particular, the machine replaces the manipulation of a heap using store-based effects with disciplined management of the evaluation stack using control-based effects. In short, state is replaced with control.To further articulate this observation, we present a simulation of call-by-need in a call-by-value language using delimited control operation

September 6th, 2019


A systematic approach to delimited control with multiple prompts

Paul Downen and Zena M. Ariola
University of Oregon

August 27th, 2019


The Science of Functional Programming
A Tutorial, with Examples in Scala

by Sergei Winitzki, Ph.D.
draft version, August 16, 2019

August 24th, 2019


Match types have similarities with closed type families in Haskell. Some differences are:

Subtyping instead of type equalities.
Match type reduction does not tighten the underlying constraint, whereas type family reduction does unify. This difference in approach mirrors the difference between local type inference in Scala and global type inference in Haskell.
No a-priori requirement that cases are non-overlapping. Uses parallel reduction instead of always chosing a unique branch.

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.
Powered by LiveJournal.com