Lambda the Ultimate

Parameterized Notions of Computation, Robert Atkey, JFP 2008.

Moggi's Computational Monads and Power et al's equivalent notion of Freyd category have captured a large range of computational effects present in programming languages. Examples include non-termination, non-determinism, exceptions, continuations, side-effects and input/output. We present generalisations of both computational monads and Freyd categories, which we call parameterised monads and parameterised Freyd categories, that also capture computational effects with parameters.

Examples of such are composable continuations, side-effects where the type of the state varies and input/output where the range of inputs and outputs varies. By also considering structured parameterisation, we extend the range of effects to cover separated side-effects and multiple independent streams of I/O. We also present two typed λ-calculi that soundly and completely model our categorical definitions — with and without symmetric monoidal parameterisation — and act as prototypical languages with parameterised effects.

Once you've programmed with monads for a while, it's pretty common to start defining parameterized families of monads -- e.g., we might define a family of type constructors for IO, in which the program type additionally tracks which files the computation reads and writes from. This is a very convenient programming pattern, but the theory of it is honestly a little sketchy: on what basis do we conclude that the indices we define actually track what we intend them to? And furthermore, why can we believe that (say) the monadic equational laws still apply? That's the question Atkey lays out a nice solution to. He gives a nice categorical semantics for indexed, effectful computations, and then cooks up lambda calculi whose equational theory corresponds to the equations his semantics justifies.

The application to delimited continuations is quite nice, and the type theories can also give a little insight into the basics of how stuff like Hoare Type Theory works (which uses parameterized monads, with a very sophisticated language of parameters).

On a slightly tangential note, this also raises in my mind a methodological point. Over the last n years, we've seen many people identify certain type constructors, whose usage is pervasive, and greatly simplified with some syntactic extensions -- monads, comonads, applicative functors, arrows, and so on. It's incredible to suggest that we have exhausted the list of interesting types, and so together they constitute a good argument for some kind of language extension mechanism, such as macros. However, all these examples also raise the bar for when a macro is a good idea, because what makes them compelling is precisely that the right syntax yields an interesting and pretty equational theory in the extended language.

Verifying Compiler Transformations for Concurrent Programs. Sebastian Burckhardt, Madanlal Musuvathi, Vasu singh.

ompilers transform programs, either to optimize performance or to translate language-level constructs into hardware primitives. For concurrent programs, ensuring that a transformation preserves the semantics of the input program can be challenging. In particular, the emitted code must correctly emulate the semantics of the language-level memory model when running on hardware with a relaxed memory model. In this paper, we present a novel proof methodology for proving the soundness of compiler transformations for concurrent programs. Our methodology is based on a new formalization of memory models as dynamic rewrite rules on event streams. We implement our proof methodology in a first-of-its-kind semi-automated tool called Traver to verify or falsify compiler transformations. Using Traver, we prove or refute the soundness of several commonly used compiler transformations for various memory models. In this process, we find subtle bugs in the CLR JIT compiler and in the JSR-133 Java JIT compiler recommendations.

The goal is to reason about the effects that different memory models may have on the validity of transformations. Program execution is modeled as an event stream, with the memory model being able to alter the event stream by swapping or eliminating events. Each concurrent execution thread produces a separate event stream. The event stream produced by the execution of the concurrent program is the (possibly altered) result of merging the event streams of each component. The validity of transformation can thus be proved relative to a specific memory model (i.e., a set of stream rewrite rules).

Traver lives here.

A Framework for Comparing Models of Computation by Edward A. Lee and Alberto Sangiovanni-Vincentelli, 1998.

We give a denotational framework (a “meta model”) within which certain properties of models of computation can be compared. It describes concurrent processes in general terms as sets of possible behaviors. A process is determinate if, given the constraints imposed by the inputs, there are exactly one or exactly zero behaviors. Compositions of processes are processes with behaviors in the intersection of the behaviors of the component processes. The interaction between processes is through signals, which are collections of events. Each event is a value-tag pair, where the tags can come from a partially ordered or totally ordered set. Timed models are where the set of tags is totally ordered. Synchronous events share the same tag, and synchronous signals contain events with the same set of tags. Synchronous processes have only synchronous signals as behaviors. Strict causality (in timed tag systems) and continuity (in untimed tag systems) ensure determinacy under certain technical conditions. The framework is used to compare certain essential features of various models of computation, including Kahn process networks, dataflow, sequential processes, concurrent sequential processes with rendezvous, Petri nets, and discrete-event systems.

The generality of the approach looks very impressive. Can anyone share first-hand experience with this framework? Would be great to see E compared to Oz!

Anna Zaks and Amir Pnueli (2008). CoVaC: Compiler Validation by Program Analysis of the Cross-Product. In Proc. 15th Symp. Formal Methods.

From the introduction:

In this paper, we present a Compiler Verification by Program Analysis of the Cross-Product framework (CoVaC ) - a novel translation validation approach, in which one constructs a comparison system - a cross-product of the source and target programs. The input programs are equivalent if and only if the comparison system satisfies a certain specification. This allows us to leverage the existing methods of proving properties of a single program instead of relying on program analysis and proof rules specialized to translation validation, used by the existing frameworks.

and

Finally, this paper reports on a prototype tool CoVaC that applies the developed framework to verification of optimizing transformations performed by LLVM 1.9 - a very aggressive open-source compiler.

UpgradeJ: Incremental Typechecking for Class Upgrades, Gavin Bierman, Matthew Parkinson and James Noble.

One of the problems facing developers is the constant evolution of components that are used to build applications. This evolution is typical of any multi-person or multi-site software project. How can we program in this environment? More precisely, how can language design address such evolution? In this paper we attack two significant issues that arise from constant component evolution: we propose language-level extensions that permit multiple, co-existing versions of classes and the ability to dynamically upgrade from one version of a class to another, whilst still maintaining type safety guarantees and requiring only lightweight extensions to the runtime infrastructure. We show how our extensions, whilst intuitive, provide a great deal of power by giving a number of examples. Given the subtlety of the problem, we formalize a core fragment of our language and prove a number of important safety properties.

There has been an energetic discussion of API evolution in the forum, so when I saw this paper I thought it might be of interest to LtU readers.

Revisiting Coroutines, by Ana Lucia de Moura and Roberto Ierusalimschy:

This paper defends the revival of coroutines as a general control abstraction. After proposing a new classification of coroutines, we introduce the concept of full asymmetric coroutines and provide a precise definition for it through an operational semantics. We then demonstrate that full coroutines have an expressive power equivalent to one-shot continuations and oneshot partial continuations. We also show that full asymmetric coroutines and one-shot partial continuations have many similarities, and therefore present comparable benefits. Nevertheless, coroutines are easier implemented and understood, specially in the realm of procedural languages. Finally, we provide a collection of programming examples that illustrate the use of full asymmetric coroutines to support direct and concise implementations of several useful control behaviors, including cooperative multitasking.

Coroutines seem to get fairly short riff in the literature, and they have only been discussed on LTU, a couple of times. Given coroutines have such a straightforward mapping to hardware, I hope they get more attention.

Coroutines show up in many different places. For instance, the inter-process communication (IPC) facilities of microkernels, like EROS, are a faithful implementation of asymmetric coroutines, with an important difference. Essentially, yield and resume must both take an explicit coroutine argument naming the coroutine respectively yield to and resume. If the coroutine to yield to is left implicit, as it is in most treatments I've seen, then coroutines become less composable since yield returns control to the innermost resume which, given abstract types, might be the wrong one.

This problem is discussed in Section 5.6, "Avoiding Interference Between Control Actions". The paper recommends tagging coroutines to match up resume/yield pairs, but the EROS IPC system provides a more direct encoding via a "resume" capability, which is a single-use coroutine used to return control directly to a client. Each subsequent invocation of the object synthesizes a new resume capability.

Taking this to the extreme implies that yield and resume can be unified into a single "invoke" operation which accepts a coroutine argument to be used in a subsequent invoke operation. Indeed, these are "symmetric coroutines". This paper suggests that symmetric coroutines are harder to understand due to the actors/CPS-like nature of the control flow.

Disciple is an explicitly lazy dialect of Haskell which includes:

• first class destructive update of arbitrary data.
• computational effects without the need for state monads.
• type directed field projections.

All this and more through the magic of effect typing.

The wiki page has more information, unfortunately there's no paper yet summarizing the ideas and results. Their effect system is quite interesting. Some of the ideas recently discussed here are implemented in Disciple.

via Haskell Cafe

Eriskay: a Programming Language Based on Game Semantics. John Longley and Nicholas Wolverson. GaLoP 2008.

We report on an ongoing project to design a strongly typed, class-based object-oriented language based around ideas from game semantics. Part of our goal is to create a powerful modern programming language whose clean semantic basis renders it amenable to work in program verification; however, we argue that our semantically inspired approach also yields benefits of more immediate relevance to programmers, such as expressive new language constructs and novel type systems for enforcing security properties of the language. We describe a simple-minded game model with a rich mathematical structure, and explain how this model may be used to guide the design of our language. We then focus on three specific areas where our approach appears to offer something new: linear types and continuations; observational equivalence for class types; and static control of the use of higher-order store.

In a substantial appendix, we present the formal definition of a fragment of our language which embodies many of the innovative features of the full language.

It's always interesting to see a new programming language strongly based on some mathematical formalism, because a language gives you a concrete example to match the abstract semantic definitions to, and game semantics is something that I've been curious about for a while.

One particularly interesting feature is that the core language has a restricted model of the heap, which controls the use of higher-order store in such a way that cycles are prohibited. This is enforced with a notion called "argument safety", which essentially prohibits storing values of higher type into fields which come from "outside" the object. This is somewhat reminiscent of the ownership disciplines found in OO verification systems like Boogie, which enforce a tree structure on the ownership hierarchy. It would be very interesting to find out whether this resemblance is a coincidence or not.

(Samson Abramsky has some lecture notes on game semantics for the very curious.)

Foundations for Structured Programming with GADTs, Patricia Johann and Neil Ghani. POPL 2008.

GADTs are at the cutting edge of functional programming and become more widely used every day. Nevertheless, the semantic foundations underlying GADTs are not well understood. In this paper we solve this problem by showing that the standard theory of datatypes as carriers of initial algebras of functors can be extended from algebraic and nested data types to GADTs. We then use this observation to derive an initial algebra semantics for GADTs, thus ensuring that all of the accumulated knowledge about initial algebras can be brought to bear on them. Next, we use our initial algebra semantics for GADTs to derive expressive and principled tools -- analogous to the well-known and widely-used ones for algebraic and nested data types -- for reasoning about, programming with, and improving the performance of programs involving, GADTs; we christen such a collection of tools for a GADT an initial algebra package. Along the way, we give a constructive demonstration that every GADT can be reduced to one which uses only the equality GADT and existential quantification. Although other such reductions exist in the literature, ours is entirely local, is independent of any particular syntactic presentation of GADTs, and can be implemented in the host language, rather than existing solely as a metatheoretical artifact. The main technical ideas underlying our approach are (i) to modify the notion of a higher-order functor so that GADTs can be seen as carriers of initial algebras of higher-order functors, and (ii) to use left Kan extensions to trade arbitrary GADTs for simpler-but-equivalent ones for which initial algebra semantics can be derived.

I found this to be a really interesting paper, because the work had an opposite effect on my opinions from what I expected. Usually, when I see a paper give a really clean semantics to an idea, I end up convinced that this is actually a good idea. However, Johann and Ghani gave a really elegant treatment of GADTs, which had the effect of making me think that perhaps Haskell-style GADTs should not be added as is to new programming languages!

This is because of the way they give semantics to GADTs as functors |C| -> C, where C is the usual semantic category (eg, CPPO) and |C| is the discrete category formed from C that retains the objects and only the identity morphisms. If I understand rightly, this illustrates that the indices in a GADT are only being used as index terms, and their structure as types is going unused. So it's really kind of a pun, arising from the accident that Haskell has * as its only base kind. This makes me think that future languages should include indices, but that these index domains should not coincide with kind type. That is, users should be able to define new kinds distinct from *, and use those as indexes to types, and these are the datatypes which should get a semantics in the style of this paper.

When Is A Functional Program Not A Functional Program?, John Longley. ICFP 1999.

In an impure functional language, there are programs whose behavior is completely functional (in that they behave extensionally on inputs) but the functions they compute cannot be written in the purely functional fragment of the language. That is, the class of programs with functional behavior is more expressive than the usual class of pure functional programs. In this paper we introduce this extended class of "functional" programs by means of examples in Standard ML, and explore what they might have to offer to programmers and language implementors.

After reviewing some theoretical background, we present some examples of functions of the above kind, and discuss how they may be implemented. We then consider two possible programming applications for these functions: the implementation of a search algorithm, and an algorithm for exact real-number integration. We discuss the advantages and limitations of this style of programming relative to other approaches. We also consider the increased scope for compiler optimizations that these functions would offer.

I like this paper because it shows how some of the most abstract bits of formal logic (realizability models of higher order logic) suggest actual programs you can write.

As a barely-related aside, even a brief look into this realizability stuff also taught me a good deal of humility -- for example, it seems that at higher types, what you can represent mathematically depends on the specific notion of computation you're using. So the mathematical consequences of the Church-Turing thesis are rather more subtle than we might initially expect. (Andrej Bauer discusses a related point in more detail in this blog post.)