Lambda the Ultimate

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.

RZ for Constructive Mathematics in Programming by Chris Stone and Andrej Bauer.

Realizability theory is not only a fundamental tool in logic and computability, but also has direct application to the design and implementation of programs: it can produce interfaces for the data structure corresponding to a mathematical theory. Our tool, called RZ, serves as a bridge between the worlds of constructive mathematics and programming. By using the realizability interpretation of constructive mathematics, RZ translates specifications in constructive logic into annotated interface code in Objective Caml. The system supports a rich input language allowing descriptions of complex mathematical structures. RZ does not extract code from proofs, but allows any implementation method, from handwritten code to code extracted from proofs by other tools.

I haven't read the paper yet, but the abstract reminded me of PADS.

Meta-Compilation of Language Abstractions, a dissertation by Pinku Surana.

High-level programming languages are currently transformed into efficient low-level code using optimizations that are encoded directly into the compiler. Libraries, which are semantically rich user-level abstractions, are largely ignored by the compiler. Consequently, library writers often provide a complex, low-level interface to which programmers "manually compile" their high-level ideas. If library writers provide a high-level interface, it generally comes at the cost of performance. Ideally, library writers should provide a high-level interface and a means to compile it efficiently.

This dissertation demonstrates that a compiler can be dynamically extended to support user-level abstractions. The Sausage meta-compilation system is an extensible source-to-source compiler for a subset of the Scheme programming language. Since the source language lacks nearly all the abstractions found in popular languages, new abstractions are implemented by a library and a compiler extension. In fact, Sausage implements all its general-purpose optimizations for functional languages as compiler extensions. A meta-compiler, therefore, is merely a shell that coordinates the execution of many external extensions to compile a single module. Sausage demonstrates that a compiler designed to be extended can evolve and adapt to new domains without a loss of efficiency.

A very interesting and detailed paper, which touches on many perennial LtU subjects, and once again shifts the line between user programs and the compiler. If you're tempted to say "this sounds like X...", then read Chapter 2, which gives a comprehensive comparison to alternative approaches, including static type inference, traditional macro systems, templates, partial evaluation, and multi-stage languages such as MetaML and MetaOCaml.

Some carefully selected quotes which I think summarize the summary quite well:

The Sausage system provides a framework for programmers to write new domain-specific optimizations and inject them into the main compiler.
...
This dissertation takes the rather extreme view that anything beyond Core Scheme is a compiler extension.

Pinku Surana will be presenting this work at a meeting of LispNYC on Feb 13th in New York City. An announcement with details of the meeting can be found here.

Ott—a tool for writing definitions of programming languages and calculi.

Ott is a tool for writing definitions of programming languages and calculi. It takes as input a definition of a language syntax and semantics, in a concise and readable ASCII notation that is close to what one would write in informal mathematics. It generates LaTeX to build a typeset version of the definition, and Coq, HOL, and Isabelle versions of the definition. Additionally, it can be run as a filter, taking a LaTeX/Coq/Isabelle/HOL source file with embedded (symbolic) terms of the defined language, parsing them and replacing them by target-system terms. For a simple example, here is an Ott source file for an untyped call-by-value lambda calculus (test10.ott), and the generated LaTeX (compiled to pdf) and (compiled to ps), Coq, Isabelle, and HOL definitions.

Most simply, the tool can be used to aid completely informal LaTeX mathematics. Here it permits the definition, and terms within proofs and exposition, to be written in a clear, editable, ASCII notation, without LaTeX noise. It generates good-quality typeset output. By parsing (and so sort-checking) this input, it quickly catches a range of simple errors, e.g. inconsistent use of judgement forms or metavariable naming conventions.

That same input can be used to generate formal definitions, for Coq, HOL, and Isabelle. It should thereby enable a smooth transition between use of informal and formal mathematics. Additionally, the tool can automatically generate definitions of functions for free variables, single and multiple substitutions, subgrammar checks (e.g. for value subgrammars), and binding auxiliary functions. (At present only a fully concrete representation of binding is supported, without quotienting by alpha equivalence.)

The distribution includes several examples, in varying levels of completeness: untyped and simply typed lambda-calculus, a calculus with ML polymorphism, the POPLmark Fsub with and without records, an ML module system taken from (Leroy, JFP 1996) and equipped with an operational semantics, and LJ, a lightweight Java fragment.

Peter Sewell and his team continue to bridge the gap between the informal and formal worlds of programming language semantics.

Several interesting papers have been published by researchers at the University of Colorado investigating ways of making end-user programming more accessible, especially to secondary-level (i.e., High School) students. In many ways, this work reminds me of the efforts of the PLT group and their excellent DrScheme software implementation, though its strong graphical leanings makes for wonderful eye candy.

I stumbled across this body of work while trying to generate some OpenGL models from Common Lisp. It turns out that most of the AgentSheets system is built on top of a DSL embedded in Common Lisp called AgenTalk. AgentTalk is implemented on top of MCL and Allegro Common Lisp. (Interestingly, an apparently independent AgentTalk appears to have been implemented on top of DrScheme.)

I found several items of note:

1. Discussion of AntiObjects as a way of designing large systems (as a foil to the Booch system.)
2. Descriptions of compelling 3-D authoring environments for non-technical users.
3. Some neat old-school Macintosh examples from the early days of AgentSheets.
4. A wonderful 3D Lisp Programming Library, the Open Agent Engine, which is used to power all of the above examples.

My only complaint about Martin (Fowler)'s talk is that he didn't mention Smalltalk and that he said that the Lisp people have been making DSLs for 20 years. I learned about them about 20 years ago, and the Lisp people had been doing it for 20 years before that, so I think they have been doing it for 40 years. Neverthless, DSLs are only starting to become a hot topic. OOPSLA has had a Domain Specific Modeling workshop for four or five years, and I'm hoping that next year it will grow into a symposium. These are ideas that need to become ubiquitous.

Ralph also mentions Intentional Software and points to Fowler's JAOO talk on Domain Specific Languages, a video of which is available online.

Second Life Faces Threat to its Virtual Economy

Groups of Second Life content creators were gathering digitally Tuesday to protest the dissemination of a program they worry could badly damage the virtual world's nascent economy.

The controversy gathered steam Monday when Linden Lab, which publishes Second Life, posted a blog alerting residents of the virtual world to the existence of a program or bot called CopyBot, which allows someone to copy any object in Second Life. That includes goods such as clothing that people purchase for their in-world avatars, and even the virtual PCs that computer giant Dell announced Tuesday it is going to sell in the digital world.

Related to this thread, especially my "Not Merely Predictable" post, as well as the various Lightweight Static Capabilities and Robust Composition threads. I'm absolutely convinced that a future language design will evolve to accomodate the development of distributed systems in which these kinds of issues are impossible to impose. Is it time to add an "object capability security" and/or "cooperation without vulnerability" (a great phrase from Mark Miller) category to LtU?

Bjarne Stroustrup. A rationale for semantically enhanced library languages. LCSD05. October 2005.

This paper presents the rationale for a novel approach to providing expressive, teachable, maintainable, and cost-effective special-purpose languages: A Semantically Enhanced Library Language (a SEL language or a SELL) is a dialect created by supersetting a language using a library and then subsetting the result using a tool that “understands” the syntax and semantics of both the underlying language and the library.

How similar or different this idea really is compared to the facilities found in PLT Scheme and other previous apporaches to this issue?

Flapjax s a functional reactive compiler and Javascript library for creating interactive web GUIs, created by Brown PLT. You can try the compiler online, or read the docs to get more of an idea of how the language works. If you've used OO style MVC before, but not functional reactive programming (FRP), take a look at Flapjax for a different, and in my opinion, cleaner approach to the same problem.

If you're familiar with FrTime you'll recognise the elements of Flapjax -- Flapjax is essentially a Javascript implementation of FrTime, and a compiler from the Flapjax language to Javascript to make writing code less verbose. The key differences compared to the Haskell FRP tradition are that FrTime is asynchronous and uses mutable state. This means behaviours (time varying values) can be sampled at any time, whereas in Haskell FRP behaviours are all sampled at the same time, and it isn't necessary to use the arrow combinators to hide accumulators. Of course it isn't all roses: the implementation is more complex, and doesn't work well in, say, a continuation based web server as mutable state will mess up resumptions of previous continuations. (Don't get the idea that this is a problem for Flapjax -- it runs on the client, not the server.)