From shift and reset to polarized linear logic

By now, shift/reset should be as popular as call/cc was ten years ago. Some think these control operators are even more important in practice than call/cc, and should be directly supported by PLs. I believe, this paper by Chung-chieh Shan will be interesting to many who loves logic and Curry-Howard isomorphism.

From shift and reset to polarized linear logic


Griffin pointed out that, just as the pure lambda-calculus corresponds to intuitionistic logic, a lambda-calculus with first-class continuations corresponds to classical logic. We study how first-class delimited continuations, in the form of Danvy and Filinski’s shift and reset operators, can also be logically interpreted. First, we refine Danvy and Filinski’s type system for shift and reset to distinguish between pure and impure functions. This refinement not only paves the way for answer type polymorphism, which makes more terms typable, but also helps us invert the continuation-passing-style (CPS) transform: any pure lambda-term with an appropriate type is beta-eta-equivalent to the CPS transform of some shift-reset expression. We conclude that the lambda-calculus with shift and reset and the pure lambda-calculus have the same logical interpretation, namely good old intuitionistic logic. Second, we mix delimited continuations with undelimited ones. Informed by the preceding conclusion, we translate the lambda-calculus with shift and reset into a polarized variant of linear logic that integrates classical and intuitionistic reasoning. Extending previous work on the lambda-µ-calculus, this unifying intermediate language expresses computations with and without control effects, on delimited and undelimited continuations, in call-by-value and call-byname settings.

Bidirectional fold and scan

Bidirectional fold and scan, O'Donnell ,J.T. In Functional Programming, Glasgow 1993, Springer Workshops in Computing.

Bidirectional fold generalises foldl and foldr to allow simultaneous communication in both directions across a list. Bidirectional scan calculates the list of partial results of a bidirectional fold, just as scanl and scanr calculate the partial results of a foldl or foldr. Mapping scans combine a map with a scan, and often simplify programs using scans. This family of functions is significant because it expresses important patterns of computation that arise repeatedly in circuit design and data parallel programming.

The biderctional fold is a bit surprising at first, but the real reason I am posting this is to encourage discussion on the connection between functional and data prallel programming.

Variables as Channels

Method mixins - written by Erik Ernst

It is quite common to describe languages with mutable state as machine-oriented, and to describe functional, logical, and other kinds of `declarative' languages as more abstract, liberated from the old-fashioned attachment to bits and memory cells. This opinion was brought to prominence with the 1977 Turing Award
speech by John Backus [...] We must recognize that the functional and other paradigms have have produced deep and useful results. However, it is our opinion that imperative languages, especially object-oriented ones, are being widely used because of their
inherent power and not because programmers are nostalgic about
writing programs in assembly language. It is not a question of abstraction or hardware concreteness, it is about safety and freedom. Restrictive communication topologies bring safety, and flexible topologies bring freedom. To substantiate this, we need to consider variables and similar concepts as communication channels, thereby making them comparable.

This paper provides an interesting perspective on the role of variables in programming. It is about a construct called method mixins, but the discussion about the role of variables in Sec. 2 is relatively independent of the specific construct proposed in the paper:

Scrap your boilerplate with class: extensible generic functions

Scrap your boilerplate with class: extensible generic functions. Ralf Laemmel and Simon Peyton Jones.

The "scrap your boilerplate" approach to generic programming allows the programmer to generic functions that can traverse arbitrary data structures, and yet have type-specific cases. However, the approach requires all the type-specific cases to be supplied at once, when the function is defined: the function is closed. In contrast, Haskell's type classes support open, or extensible functions, that can be extended with new type-specific cases as new data types are defined. In this paper we show how to extend the scrap-your-boilerplate approach to support this open style. On the way we demonstrate the desirablility of abstraction over type classes, and the usefulness of recursive dictionaries.

If you haven't been paying attention, this is your chance to learn about the "scrap your boilerplate" approach to generic programming in Haskell. We mentioned and discussed the earlier papers in the series.

Like many of Peyton Jones's papers this one is an enlightening exploration of language design.

Differentiating Data Structures

This paper was mentioned here before, but not on the home page.

It deserves to get more attention, since it is quite cool.

Warning: This one isn't for the faint of heart, and uses scary terms like polynomial functors, initial algebras and terminal coalgebras, constructive set theory and more...

Haskell for C Programmers

Many people are accustomed to imperative languagues, which include C, C++, Java, Python, and Pascal....For [beginning] computer science students,...Haskell is weird and obtuse....This tutorial assumes that the reader is familiar [only] with C/C++, Python, Java, or Pascal. I am writing for you because it seems that no other tutorial was written to help students overcome the difficulty of moving from C/C++, Java, and the like to Haskell.

I write this assuming that you have checked out...the Gentle Introduction to Haskell, but...still don't understand what's going on....

Haskell is not 'a little different,' and will not 'take a little time.' It is very different and you cannot simply pick it up, although I hope that this tutorial will help.

If you play around with Haskell, do not merely write toy programs. Simple problems will not take advantage of Haskell's power. Its power shines mostly clearly when you...attack difficult tasks....Haskell's tools...dramatically simplify your code....

I am going to put many pauses in this tutorial because learning Haskell hurt a lot, at least for me. I needed breaks, and my brain hurt while I was trying to understand....

Now I'm working on a video game in Haskell...and we've written a short tutorial...on HOpenGL....

Haskell has both more flexibility and more control than most languages. Nothing that I know of beats C's control, but Haskell has everything C does unless you need to control specific bytes in memory. So I call Haskell powerful, rather than just 'good.'

I wrote this tutorial because Haskell was very hard for me to learn, but now I love it...."Haskell is hard!" "You can't write code the way I know how!" "My brain hurts!" "There aren't any good references!" That's what I said when I was in college. There were good references, but they didn't cover the real problem: coders know C.

New explorers might enjoy Eclipse IDE support (version 3.1M7 or later only). Old hands might help improve it.

Haskell compiles to C (cf. JHC) and machine code.

Generic Accumulations: Battery-powered Bananas

For those who do not think that "catamorphism" sounds scary, Generic Accumulations paper presents a new flavor of fold: fold with accumulators (afold).

You might be acquainted with its cousin - pfold, or fold with parameters. Both come from the family of comonadic fold.

A homepage of Alberto Pardo contains more information on them.

PS: if you are new to fold or bananas/lenses, LtU papers page has a couple of introductory links.


jhc is a haskell compiler which aims to produce the most efficient programs possible via whole program analysis and other optimizations.

This seems like an interesting project, for example: Region Inferencing, Compilation by transformation with 2 general intermediate languages, very modern design, using rank-n polymorphism, monad transformers, generic programing, and existential types.

Note, howver, that there are quite a few problems (scaling, memory leaks, etc.)

Maybe some of you might want to offer a helping hand...

Datatype Laws without Signatures

Datatype Laws without Signatures
Using the well-known categorical notion of `functor' one may define the concept of datatype (algebra) without being forced to introduce a signature, that is, names and typings for the individual sorts (types) and operations involved. This has proved to be advantageous for those theory developments where one is not interested in the syntactic appearance of an algebra.

Does it sound like "a module without a signature"?

If you like programming with bananas, lenses, and other weird things you might like this paper as well.

PS: OTOH, if you are sceptic about bialgebraic programming, then dialgebraic is definitely not for you.

Y in haskell

From the Haskell mailing list.

People often wonder about Y in Haskell, so I think it is worth to have this link in the archive. Nothing new here for Haskell mavens, though.

XML feed