Lambda the Ultimate

If you're a GHC user, the Glasgow Haskell Compiler HeadQuarters needs your feedback! See Simon Peyton-Jones original message, or go directly to the user survey. Here's a quote from the original message:

We'd like to hear from *absolutely everyone* who uses GHC: whether you
are a first-year undergraduate or a famous professor; whether you use
GHC for industrial applications or recreation; whether you use
higher-rank polymorphism or have only just learned what functional
programming is. Everyone!

We'll use the information to guide our future priorities, and we'll
publish some kind of summary of what we learn in due course. It's all
anonymous, of course, unless you choose to say who you are.

Ωmega is a new programming language by Tim Sheard which is descended from Haskell and adds new facilities for defining static type constraints, such as allowing "users to write functions at the level of types, and then use those functions in the type of functions at value level". It also has "equality qualified types". See also Programming with Static Invariants in Omega and the manual for more information. Mentioned previously (in passing) on LtU.

Metaphor is a strongly-typed, multi-stage, object-oriented programming language. Metaphor is based on a subset of C# and is extended with multi-stage programming constructs in the style of MetaML or MetaOCaml. Metaphor is implemented as a compiler on the .NET CLR.

Metaphor features a static type system for object-oriented reflection operations (i.e. run-time type analysis). This allows the reflection system to be safely incorporated into the language’s staging constructs and thus allows the generation of code based on the structure of types.

A lot of language theory goes past here on Lambda the Ultimate, but we rarely see that theory directly impacting commercial programmers.

I'm a great fan of theoretical concepts like arrows, but at the same time I'm a self-employed programmer interested in solving my clients' problems.

Pugs is notable in that it profitably uses recent developments such as GADTs and Template Haskell for an implementation of Perl6.

I recently became a regular on the #perl6 irc channel and soon after joined the list of committers.

In just a few days I've seen a lot. I've seen enthusiastic members of the Perl community learning Haskell. I've seen myself learning Perl. I've also seen how daily Perl programmers work with abstractions like monad transformers. I've seen how some structures are easy to extend for programmers new to both the Pugs codebase and Haskell.

The Pugs project was started 64 days ago by Autrijus Tang, as an exercise while reading TaPL. Pugs already includes network and threading primitives. New tests and code are add at an amazing rate, as evidenced by the smoke tests.

I don't know if I'll end up using Perl after Pugs is written, but I am learning how to practice the theory of programming language design and implementation.

Interesting paper from PyCon 2003 (so yes, it's old news - but new on Lambda, as far as I can see): UCPy: Reverse-Engineering Python.

The project partly entails replacing the "CISC-style" Python VM with a much smaller "RISC-style" VM. The authors' comments on this decision are worth considering in the light of recent discussions about the design of the Parrot VM.

Along the lines of the quine discussion happening in another thread, Manfred von Thun wrote a new page for the Joy site, Reproducing Programs implement Lazy Lists. This connects nicely with Jeremy Gibbons spigot algorithms paper, one example of which is his IOHCC 2004 submission PiSpigot.

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

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.

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.

This weekend, I took another crack at trimming microseconds off the common-case path for generic function execution, and succeeded in dropping the excution time from 13.2 microseconds to just over 9.8. (Which is about 9 microseconds overhead added relative to a hand-optimized Python version of the same trivial function.) Along the way, however, I realized a couple of surprising things about Python performance tuning.

An amusing story that tells you something about Python's implementation.

The discussion of closures is of particular interest...