Lambda the Ultimate

Towards efficient, typed LR parsers, François Pottier and Yann Régis-Gianas. In ACM Workshop on ML, March 2006.

The LR parser generators that are bundled with many functional programming language implementations produce code that is untyped, needlessly inefficient, or both. We show that, using generalized algebraic data types, it is possible to produce parsers that are well-typed (so they cannot unexpectedly crash or fail) and nevertheless efficient. This is a pleasing result as well as an illustration of the new expressiveness offered by generalized algebraic data types.

Abstract Interface Types in GNAT: Conversions, Discriminants, and C++. Javier Miranda and Edmond Schonberg.

Ada 2005 Abstract Interface Types provide a limited and practical form of multiple inheritance of specifications. In this paper we cover the following aspects of their implementation in the GNAT compiler: interface type conversions, the layout of variable sized tagged objects with interface progenitors, and the use of the GNAT compiler for interfacing with C++ classes with compatible inheritance trees.

The addition of interface types, of the type found in Java, to Ada2005 presented compiler writers with an implementation challenge. This is a third paper in a series describing the implementation of interfaces in the GNAT Ada compiler (an earlier paper dealt with synchronized interfaces, an interesting special case).

The present paper deals mainly with issues caused by interface type conversions, and the related data layout issues. Of special interest is section 6 which shows how to write a C++/Ada multi-language program, in which method calls can be dispatched across language boundaries. Handling the multiple inheritance in the C++ code in this example is possible because the base classes have only pure virtual functions.

Cforall is a language design extending ISO C.

Cforall extends the C type-system using overloading, parametric polymorphism, and type generators. … [The] Cforall type system is based on parametric polymorphism, the ability to declare functions with type parameters, rather than an object-oriented type system.

NixOS is a Linux distribution based on Nix, a purely functional package management system. NixOS is an experiment to see if we can build an operating system in which software packages, configuration files, boot scripts and the like are all managaed in a purely functional way, that is, they are all built by deterministic functions and they never change after they have been built. Such an operating system should have all the nice characteristics that the Nix package manager has.

Here are links to:

• the Nix package manager webpage,
• the NixOS webpage, and
• Eelco Dolstra's PhD thesis, The Purely Functional Software Deployment Model.

I found this an extremely readable thesis, light on math but high on insight. I now have an entirely new way of thinking about components and the filesystem, and that's really cool. I'd be very interested in hearing what people with serious deployment/sysadmin experience think about this approach.

(Thanks to Gavin Mendel-Gleason and Martin Bravenboer for posting the original links in the discussions page!)

Having been entirely too dismissive of one of Nick Benton's papers before, it seems only fitting that I should attempt expiation for my sins by discussing Formalizing and Verifying Semantic Type Soundness of a Simple Compiler:

We describe a semantic type soundness result, formalized in the Coq proof assistant, for a compiler from a simple imperative language with heap-allocated data into an idealized assembly language. Types in the high-level language are interpreted as binary relations, built using both second-order quantification and a form of separation structure, over stores and code pointers in the low-level machine.

I found this work striking for its strong defense of the utility of semantic, vs. syntactic, type soundness, and for its use of logical relations vs. unary predicates. I could swear that I recently read another paper making quite similar observations about semantic vs. syntactic type soundness. I'm not sure which paper it was, but regardless, there seems to me to be a great deal of overlap of insight and, to a lesser extent, approach, with A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language, and of course by extension to Leroy's work on formalizing big-step operational semantics, allocation, etc. Finally we have the very exciting news about progress on a mechanized metatheory for Standard ML, in Twelf. It's a very exciting time for mechanized metatheory! I'd love to get at least Nick Benton, Adam Chlipala, Xavier Leroy, and Tim Sweeney in a room for a few months so they could create the Next Mainstream Programming Language in Coq. Of course, we have Dr. Benton, Mr. Chlipala, and Mr. Sweeney right here on LtU... :-)

Update: Mea culpa; the paper I had in mind was A Very Modal Model of a Modern, Major, General Type System. It would seem that Dr. Benton, Mr. Chlipala, and Dr. Appel and colleagues have arrived at quite similar perspectives on good approaches to mechanizing metatheory for very interesting programming language design efforts.

Andreas Rossberg has updated HaMLet, a reference implementation of SML in SML, to support many of the suggestions for Successor ML (sML). The nice thing about implementing a PL in a high level PL (especially a metacircular implementation) is that it makes it easier to try out new language features.

HaMLet-S is a spin-off devoted to Successor ML (www.successor-ml.org). It incorporates a number of preliminary proposals and is a testbed and sort of a personal vision of where SML could go. Version 1.3/S4 features the following:

• Extensible records.
• More expressive pattern matching.
• Views (a la Wadler and Okasaki).
• Higher-order modules and nested signatures.
• Local and first-class modules.
• Miscellaneous fixes to known issues with SML.

A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language

I present a certified compiler from simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler and the terms of its several intermediate languages are given dependent types that guarantee that only well-typed programs are representable. Thus, type preservation for each compiler pass follows without any significant "proofs" of the usual kind. Semantics preservation is proved based on denotational semantics assigned to the intermediate languages. I demonstrate how working with a type-preserving compiler enables type-directed proof search to discharge automatically large parts of the proof obligations.

Software/proof source code and documentation

Slides are available from a talk I gave at the Projet Gallium seminar at INRIA Rocquencourt, in OpenOffice and PDF formats.

I found this while attempting to follow up on this post. The approach taken here—dependently-typed ASTs and denotational semantics—and the observation that, carried to its logical conclusion, the result is typed intermediate and assembly languages, proof-carrying code, etc. suggests to me a connection to this work. It also seems to offer a denotational counterpoint to Leroy's coinductive big-step operational semantics, also done in Coq. Fascinating stuff.

Pico Lisp: A Radical Approach to Application Development describes a minimalist Lisp interpreter which has been used to build real applications for ~20 years. If you ignore the tendency toward self-aggrandizing, there's some food for thought here. Pico Lisp only has native support for symbols, integers, and lists (no arrays, no structures), and is implemented as a straightfoward interpreter. Yet in the benchmarks (usual disclaimers here), Pico Lisp fares well against a compiled Lisp. Is there a case to be made for ultra lean and mean interpreters as a viable alternative to compilers?

Concoqtion: Indexed Types Now!

Almost twenty years after the pioneering efforts of Cardelli, the programming languages community is vigorously pursuing ways to incorporate F_ω-style indexed types into programming languages. This paper advocates Concoqtion, a practical approach to adding such highly expressive types to full-fledged programming languages. The approach is applied to MetaOCaml using the Coq proof checker to conservatively extend Hindley-Milner type inference. The implementation of MetaOCaml Concoqtion requires minimal modifications to the syntax, the type checker, and the compiler; and yields a language comparable in notation to the leading
proposals. The resulting language provides unlimited expressiveness in the type system while maintaining decidability. Furthermore, programmers can take advantage of a wide range of libraries not only for the programming language but also for the indexed types. Programming in MetaOCaml Concoqtion is illustrated with small examples and a case study implementing a statically-typed domain-specific language.

The follow-up to Concoqtion: Mixing Indexed Types and Hindley-Milner Type Inference, discussed earlier. Good stuff.

Update: There's now a public Concoqtion web site!

Josh, does this answer your question? :-)

The Design and Implementation of a Dataflow Language for Scriptable Debugging, Guillaume Marceau, Gregory H. Cooper, Jonathan P. Spiro, Shriram Krishnamurthi, and Steven P. Reiss.

Debugging is a laborious, manual activity that often involves the repetition of common operations. Ideally, users should be able to describe these repetitious operations as little programs. Debuggers should therefore be programmable, or scriptable. The operating environment of these scripts, however, imposes interesting design challenges on the programming language in which these scripts are written.

This paper presents our design of a language for scripting debuggers. The language offers powerful primitives that can precisely and concisely capture many important debugging and comprehension metaphors. The paper also describes a pair of debuggers, one for Java and the other for Scheme, built in accordance with these principles. The paper includes concrete examples of applying this debugger to programs.

We've seen a paper on compiling dataflow languages, so here's one on an interesting application.