Lambda the Ultimate

Aspect-oriented programming is emerging as a powerful tool for system design and development. In this paper, we study aspects as primitive computational entities on par with objects, functions and horn-clauses. To this end, we introduce μABC, a name-based calculus, that incorporates aspects as primitive. In contrast to earlier work on aspects in the context of object-oriented and functional programming, the only computational entities in μABC are aspects. We establish a compositional translations into μABC from a functional language with aspects and higher-order functions. Further, we delineate the features required to support an aspect-oriented style by presenting a translation of μABC into an extended π-calculus.

This message presents polymorphic functions that derive a term for a given type -- for a class of fully polymorphic functions: proper and improper combinators.

Oleg's converter can let us `visualize' what a function with a particular type may be doing. It can be helpful in understanding functions written in point-free style.

And to top it off, we are shown how to do SLD resolution using Haskell typeclasses...

Interesting sounding projects...

I am busy, but where are all the other editors? Step up to the plate, and post something!

It was with some shock that I read (via Slashdot) about Adobe's Open Source presentation engine (and layout system). In my experience, very few companies take much stock in writing generic systems that leverage the body of computer science.

So, I was quite pleased to read Sean Parent's comments:

The most ambitious library, Adam, stems from the intuition that the logic behind a simple human interface can be distilled to a function:

f(x) -> x'

The code providing this functionality accounts for a third of Adobe's code base and nearly half of the bugs found during development. Obviously these functions are not so simple, at least not as currently expressed. The apparent complexity is due to a high degree of interconnected variables. Event handling code alone does not have enough context for solving such systems.

The next jaw-dropping tidbit came a few lines later:

Still, I am convinced that writing correct, high performance, and feature rich systems can be orders of magnitude simpler than it currently is. By my estimate, 70% of Adobe's current code base could be better represented declaratively. The remaining imperative logic could be largely generic - reused both within and across Adobe's applications. Realizing even a fraction of this potential would open up a world of opportunities. I strongly suspect the proportions are similar throughout the industry.

The website provides an overview of exactly what has been released:

Adam is a modeling engine and declarative language for describing constraints and relationships on a collection of value, typically the parameters to an application command. When bound to a human interface (HI) Adam provides the logic that controls the HI behavior. Adam is similar in concept to a spreadsheet or a forms manager. Values are set and dependent values are recalculated. Adam provides facilities to resolve interrelated dependencies and to track those dependencies, beyond what a spreadsheet provides.

Eve consists of a declarative language and layout engine for constructing an HI. The layout engine in Eve takes into account a rich description of UI elements to achieve a high quality layout - rivaling what can be achieved with manual placement. A single HI description in Eve suffices for multiple OS platforms and languages. This document describes Eve2, the latest version of Eve. Eve2 was developed to work with Adam and to incorporate many improvements that have been requested since Eve1 was written.

It is important to note that Adam and Eve do not constitute a traditional application framework. They are component libraries which can be incorporated into a number of environments. They can be used together, or independently, but must be combined with other facilities to construct an application. Nearly all of the components which comprise Adam and Eve can also be used independently and are documented as part of ASL.

Sadly, my experience with Adobe's products extends only to their Acrobat Reader software, so I can't claim from personal experience that they have achieved their aim of writing stable software.

However, the fact that top-level architects at Adobe are cognizant of declarative paradigms and generic programming gives me new hope in the industry.

A computer science textbook that wasn't discussed here before, and that many of you may haven't encountered yet.

The basic approach is summarized in the title of the authors presentation From Nand to Tetris in 12 Steps (3.5 MB, Powerpoint).

I am sure LtU readers will find a lot to complain about (they authors build an OO language...), but I am fond of the hands on approach, which is kind of similar to the approach taken by our favorites: SICP, CTM, EOPL etc.

Update: The published book is The Elements of Computing Systems, Building a Modern Computer from First Principles. Noam Nisan and Shimon Schocken, MIT Press, 2005.

LtU now has a complete set of RSS feeds, covering front page stories, discussion forum topics, and comments:

• http://lambda-the-ultimate.org/node/feed - Front page stories (the original feed, which hasn't changed)
• http://lambda-the-ultimate.org/taxonomy/feed/or/1,2 - Discussion forum topics
• http://lambda-the-ultimate.org/crss - All comments, whether posted to front page stories or the discussion forum

The first two feeds above include only top-level stories and topics, and the comment feed includes only comments. If you want RSS for all story and forum content posted on the site, including comments, then you need all three feeds.

There are a couple of known limitations of these feeds right now, which should be corrected soon:

• The comment feed does not specify which story/thread a comment belongs to.
• The front page and forum feeds do not specify who posted a story or new forum topic.

We haven't yet added any menu links or icons for the new feeds. We're interested in getting some feedback on this three-feed approach: would it be preferable to have two feeds, one for both front page and forum items, without comments, and another which includes all content including comments? The current setup follows the line of least resistance in terms of implementation, but if there are any strong preferences we'll take that into account in the upcoming upgrade of Drupal.

www.stepanovpapers.com is a collection of Alex Stepanov's papers, class notes, and source code, covering generic programming and other topics. This may be of interest to those wanting to understand how the programming style exhibited by the C++ Standard Template Library evolved. Credit goes to Mat Marcus for obtaining the domain name and ISP account, and to Dave Musser, Meng Lee, Jim Dehnert, Jeremy Siek, Mat Marcus, and Alex Stepanov for scrounging through their files to find copies of the material.

This is a tutorial on using type-indexed embedding projection pairs when writing interpreters in statically-typed functional languages. The method allows (higher-order) values in the interpreting language to be embedded in the interpreted language and values from the interpreted language may be projected back into the interpreting one. This is particularly useful when adding command-line interfaces or scripting languages to applications written in functional languages. We first describe the basic idea and show how it may be extended to languages with recursive types and applied to elementary meta-programming. We then show how the method combines with Filinski's continuation-based monadic reflection operations to define an extensional version of the call-by-value monadic translation and hence to allow values to be mapped bidirectionally between the levels of an interpreter for a functional language parameterized by an arbitrary monad. Finally, we show how SML functions may be embedded into, and projected from, an interpreter for an asynchronous pi-calculus via an extensional variant of a standard translation from lambda into pi.

Another paper from Nick Benton.

Like the previous one this paper is dense and detailed, but this time there are some useful practical techniques that may come handy next time you build a DSL in a functional language.

Greg Restall is

writing a book, entitled Proof and Counterexample (or PnC for short). It's on logic viewed through the lens of proof theory. In particular, it covers natural deduction, sequent calculus, normalisation and cut-elimination. It's designed to both be state-of-the-art reseearch on these topics, together with an introduction appropriate for an advanced undergraduate. (We'll see how that works. I'll be test-driving the material with honours students from February to June in 2005.)

These pages will contain all sorts of different material about the book: comments, discussion, pointers to related material, and anything else that the community behind this site sees fit to write.

Newcomers to the field might wonder why this is relevant to programming languages, and some readers would regard this as pointless theory...

But if you are one of us guys excited by Curry-Howard, you might enjoy this wiki a lot.

We show how some classical static analyses for imperative programs, and the optimizing transformations which they enable, may be expressed and proved correct using elementary logical and denotational techniques. The key ingredients are an interpretation of program properties as relations, rather than predicates, and a realization that although many program analyses are traditionally formulated in very intensional terms, the associated transformations are actually enabled by more liberal extensional properties. We illustrate our approach with formal systems for analysing and transforming while-programs. The first is a simple type system which tracks constancy and dependency information and can be used to perform dead-code elimination, constant propagation and program slicing as well as capturing a form of secure information flow. The second is a relational version of Hoare logic, which significantly generalizes our first type system and can also justify optimizations including hoisting loop invariants. Finally we show how a simple available expression analysis and redundancy elimination transformation may be justified by translation into relational Hoare logic.

Not really exciting as such, but this technical report version of the POPL 2004 paper includes most of the proofs, which some might find helpful.