Welcome to Roshan's homepage...

PDF

Every functional programmer knows about sum and product types, a+b and a*b respectively. Negative and fractional types, a-b and a/b respectively, are much less known and their computational interpretation is unfamiliar and often complicated. We show that in a programming model in which information is preserved (such as the model introduced in our recent paper on `Information Effects'), these types have particularly natural computational interpretations. Intuitively, values of negative types are values that flow ``backwards'' to satisfy demands and values of fractional types are values that impose constraints on their context. The combination of these negative and fractional types enables greater flexibility in programming by breaking global invariants into local ones that can be autonomously satisfied by a subcomputation. Theoretically, these types give rise to two function spaces and to two notions of continuations, suggesting that the previously observed duality of computation conflated two orthogonal notions: an additive duality that corresponds to backtracking and a multiplicative duality that corresponds to constraint propagation.

PDF

In our previous work [RC'11, POPL'12], we developed a reversible programming language and established that every computation in it is a (partial) isomorphism that is reversible and that preserves information. The language is founded on type isomorphisms that have a clear categorical semantics but that are awkward as a notation for writing actual programs, especially recursive programs. This paper remedies this aspect by presenting a systematic technique for developing a large and expressive class of reversible recursive programs, that of logically reversible small-step abstract machines. In other words, this paper shows that once we have a logically reversible machine in a notation of our choice, expressing the machine as an isomorphic interpreter can be done systematically and does not present any significant conceptual difficulties. Concretely, we develop several simple interpreters over numbers and addition, move on to tree traversals, and finish with a meta-circular interpreter for our reversible language. Generally, this gives us a means of developing large reversible programs with the ease of reasoning at the level of a conventional small-step semantics.

PDF Slides

Computation is a physical process which, like all other physical processes, is fundamentally reversible. From the notion of type isomorphisms, we derive a typed, universal, and reversible computational model in which information is treated as a linear resource that can neither be duplicated nor erased. We use this model as a semantic foundation for computation and show that the ``gap'' between conventional irreversible computation and logically reversible computation can be captured by a type-and-effect system. Our type-and-effect system is structured as an arrow metalanguage that exposes creation and erasure of information as explicit effect operations. Irreversible computations arise from interactions with an implicit information environment, thus making them a derived notion, much like open systems in Physics. We sketch several applications which can benefit from an explicit treatment of information effects, such as quantitative information-flow security and differential privacy.

PDF Slides

PDF Slides

We develop a reversible programming language from elementary mathematical and categorical foundations. The core language is based on isomorphisms between finite types: it is complete for combinational circuits and has an elegant semantics in dagger symmetric monoidal categories. The categorical semantics enables the definition of canonical and well-behaved reversible loop operators based on the notion of traced categories. The extended language can express recursive reversible algorithms on recursive types such as the natural numbers, lists, and trees. Computations in the extended language may diverge but every terminating computation is still reversible.

Yield, the Control Operator : Applications and a Conjecture. PDF.
Yield, the control operator: Exploring Session Types. Slides.

PDF Slides

Many mainstream languages have operators named yield that share common semantic roots but differ significantly in their details. We present the first known formal study of these mainstream yield operators, unify their many semantic differences, adapt them to a functional setting, and distill the operational semantics and type theory for a generalized yield operator. The resultant yield, with its delimiter run, turns out to be a delimited control operator of comparable expressive power to shift-reset, with translations from one to the other. The mainstream variants of yield turn out to be one-shot or linearly used restrictions of delimited continuations. These connections may serve as a means of transporting ideas from the rich theory on delimited continuations to mainstream languages which have largely shied away from them. Dually, the restrictions of the various existing yield operations may be treated as shift-reset variants that have found mainstream acceptance and thus worthy of study.

PDF
Older GC Notes on haskell.org

We present a parallel generational-copying garbage collector implemented for the Glasgow Haskell Compiler. We use a block-structured memory allocator, which provides a natural granularity for dividing the work of GC between many threads, leading to a simple yet effective method for parallelising copying GC. The results are encouraging: we demonstrate wall-clock speedups of on average a factor of 2 in GC time on a commodity 4-core machine with no programmer intervention, compared to our best sequential GC.