Shifting The Stage
Stc
Date: 2008-12-04
Time: 11:45
Room: BBL room 471
Speaker: Chung-chieh Shan (Rutgers University)
(joint work with Yukiyoshi Kameyama and Oleg Kiselyov)
Title: Shifting the Stage: Staging with Delimited Control
Abstract
It is often hard to write programs that are efficient yet reusable. For
example, an efficient implementation of Gaussian elimination should
be specialized to the structure and known static properties of the
input matrix. The most profitable optimizations, such as choosing the
best pivoting or memoization, cannot be expected of even an advanced
compiler because they are specific to the domain, but expressing these
optimizations directly makes for ungainly source code. Instead, a
promising and popular way to reconcile efficiency with reusability is
for a domain expert to write code generators.
Two pillars of this approach are types and effects. Typed multilevel
languages such as MetaOCaml ensure
safety: a well-typed code generator
neither goes wrong nor generates code that goes wrong. Side effects
such as state and control ease
correctness: an effectful generator
can resemble the textbook presentation of an algorithm, as is familiar
to domain experts, yet insert
let for memoization and
if for
bounds-checking, as is necessary for efficiency. However, adding
effects blindly renders multilevel types unsound.
We introduce the first two-level calculus with control effects and a
sound type system. We give small-step operational semantics as well
as a continuation-passing style (CPS) translation. For soundness,
our calculus restricts the code generator's effects to the scope of
generated binders. Even with this restriction, we can finally write
efficient code generators for dynamic programming and numerical methods
in direct style, like in algorithm textbooks, rather than in CPS or
monadic style.
--
AndresLoeh - 24 Oct 2008
