Lambda the Ultimate

This post is triggered by Jules asking, essentially, how could FRP support imperative structures? Part of the answer is about interface -- a command becomes an input stream of commands, which is a common pattern in systems like Max/MSP, and most FRP systems also provide mutable reactive cells (... a worthwhile topic for another day). More interesting is when we want a particular imperative implementation that the automatic incrementalizer wouldn't have picked, such as a hand-tuned one in a lower-level language. Sometimes, a reactive language supports interfacing with alternative implementations in other languages automatically, as in Crossing State Lines: Adopting OO Frameworks to Functional Reactive Languages, but, as long as the incrementalization algorithm supports foreign computations, even language users can do it (e.g., Flapjax supports manual lifting of the DOM, I also did arrays, etc.).

The following recent paper, Traceable Data Types for Self-Adjusting Computation, can be interpreted as an explanation of why it has been sensible performance-wise for an FRP system like Flapjax to lift a library like the DOM: in a typed setting, the library is an ADT that has been tuned to take care of its own incrementalization and thus we just need a bit of glue to lift it:

In this paper, we extend dependence-tracing to work at the granularity of the query and update operations of arbitrary (abstract) data types, instead of just reads and writes on memory cells. This can significantly reduce the number of dependencies that need to be kept in the trace and followed during an update. We define an interface for supporting a traceable version of a data type, which reports the earliest query that depends on (is changed by) revising operations back in time, and implement several such structures, including priority queues, queues, dictionaries, and counters. We develop a semantics for tracing, extend an existing self-adjusting language, ∆ML, and its implementation to support traceable data types, and present an experimental evaluation by considering a number of benchmarks. Our experiments show dramatic improvements on space and time, sometimes by as much as two orders of magnitude.

A little more out there, and why I liked this paper, is its typed phrasing allows you to reduce the typical lifting+FFI approach for automatic incrementalization of general programs to being an instance of the the expression problem.

“An intuitionistic logic that proves Markov's principle”, Hugo Herbelin, LICS 2010.

We design an intuitionistic predicate logic that supports a limited amount of classical reasoning, just enough to prove a variant of Markov’s principle suited for predicate logic.

At the computational level, the extraction of an existential witness out of a proof of its double negation is done by using a form of statically-bound exception mechanism, what can be seen as a direct-style variant of Friedman’s A-translation.

Markov's principle is an axiom of "Russian constructivism". It says that if P is a decidable predicate (i.e., the formula ∀x. P(x) or ¬P(x) is constructively provable), then if we know that P is not always false (ie ¬(∀x. ¬P(x))), then there exists an x such that P holds (ie ∃x. P(x)).

One operational way of understanding this axiom is that it says is that if we know P is not always false (on, say, the natural numbers), we can find an element for which it is true with a while-loop: check to see if 1 is true, and then check to see if 2 is true, and so on, stopping when you hit a number for which it holds. This means that Markov's principle is a principle of unbounded search, and as a result it has controversial status in intuitionistic mathematics -- should we regard a program with a non-constructive termination proof as a constructively terminating program? (The answer is, as usual, "it depends": in different applications you can want it or not.)

However, just chucking an axiom like ¬(∀x. ¬P(x)) → ∃x. P(x) into your proof rules is not very nice from a proof-theoretic perspective. It mixes up a bunch of different logical connectives, and adding it as an axiom will break things like the cut-elimination theorem for sequent calculus.

In this paper, Herbelin exploits (a) the fact that Markov's principle is a (mildly) classical principle of reasoning, and (b) the fact that classical logic is connected with control operators like continuations, to give a logic which is proof-theoretically well-behaved, but which supports Markov's principle. The trick is to add first-class continuations, but only for value types (ie, you can throw products and sums, but not functions).

What I find surprising is that this same class of restriction also arises in another paper on control operators at LICS -- Noam Zeilberger's paper "Polarity and the Logic of Delimited Continuations" uses it too. (This paper deserves a post here too.)

Here's a little sausage making article for JVM language implementors. In Compiling Structural Types on the JVM: A Comparison of Reflective and Generative Techniques from Scala’s Perspective, Gilles Dubochet and Martin Odersky describe

Scala’s compilation technique of structural types for the JVM. The technique uses Java reflection and polymorphic inline caches. Performance measurements of this technique are presented and analysed. Further measurements compare Scala’s reflective technique with the “generative” technique used by Whiteoak to compile structural types. The article ends with a comparison of reflective and generative techniques for compiling structural types. It concludes that generative techniques may, in specific cases, exhibit higher performances than reflective approaches, but that reflective techniques are easier to implement and have fewer restrictions.

There's no discussion of the the proposed JVM "method handles" and whether they might be an even better solution than runtime reflection.

Whiteoak was mentioned previously on LtU.

The introduction of Helios (Eclipse 3.6) included the release of version 1.0 of Xtext - Language Development Framework.

With Xtext you can easily create your own programming languages and domain-specific languages (DSLs). The framework supports the development of language infrastructures including compilers and interpreters as well as full blown Eclipse-based IDE integration.

Given a grammar, Xtext derives a parser and an IDE with syntax highlighting, code completion, code folding, outline view, real-time error reporting, quick fixes among other standard IDE features. The models then can be used as an EMF Resource(ie as an interpreter) or with a little more work they can be used to generate code as well.

Check out the video clips on their website or the Webinar for a more detailed look.

Why Undergraduates Should Learn the Principles of Programming Languages

The linked document is the first public release of a document discussing the value of programming languages principles for undergraduate CS majors. The intended audience is computer scientists who are not specialists in programming languages. Please leave comments on how well you believe it meets its goals and with suggestions for improvements.

Abstract: Undergraduate students obtain important knowledge and skills by studying the pragmatics of programming in multiple languages and the principles underlying programming language design and implementation. These topics strengthen students' grasp of the power of computation, help students choose the most appropriate programming model and language for a given problem, and improve their design skills. Understanding programming languages thus helps students in ways vital to many career paths and interests.

It would be nice if people interested in this as much as Kim Bruce could actively post such stuff to LtU as contributing editors, hint hint professors...

Edit: In case Kim Bruce is listening, I found this link today via Hacker News posting. There are some comments there, too.

Intel Concurrent Collections...provides a mechanism for constructing [programs] that will execute in parallel while allowing the application developer to ignore issues of parallelism such as low-level threading constructs or the scheduling and distribution of computations. The model allows the programmer to specify high-level computational steps including inputs and outputs without imposing unnecessary ordering on their execution... Data is either local to a computational step or it is explicitly produced and consumed by them. An application in this programming model supports multiple styles of parallelism (e.g., data, task, pipeline parallel). While the interface between the computational steps and the runtime system remains unchanged, a wide range of runtime systems may target different architectures (e.g., shared memory, distributed) or support different scheduling methodologies (e.g., static or dynamic).

In short CnC purports to be a "a graph-based data-flow-esque deterministic parallel programming model". An open-source Haskell edition of the software was recently released on Hackage.

A series of blog posts describe the implementation: #1, #2, #3, #4, #5 (the last post links to a draft paper).

Personally, I would have preferred a more concise and down to earth description on the whole thing. If you have experiences to share, please do.

OpenSCAD is a software for creating solid 3D CAD objects... OpenSCAD is not an interactive modeller. Instead it is something like a 3D-compiler that reads in a script file that describes the object and renders the 3D model from this script file (see examples below). This gives you (the designer) full control over the modelling process and enables you to easily change any step in the modelling process or make designes that are defined by configurable parameters.

In days gone by I used to post examples demonstrating the power of DSLs over GUIs. This is a nice example I came across recently. The scripting approach may be useful, of course, to 2D CAD as well. Here is an amusing example.

Maybe the analog computing DSL I fantasized about should output SCAD scripts instead of compiling directly to g-code...

We present the lambda_m-calculus, a semantics for a language of hygienic macros with a non-trivial theory. Unlike Scheme, where programs must be macro-expanded to be analyzed, our semantics admits reasoning about programs as they appear to programmers. Our contributions include a semantics of hygienic macro expansion, a formal definition of α-equivalence that is independent of expansion, and a proof that expansion preserves α-equivalence. The key technical component of our language is a type system similar to Culpepper and Felleisen's "shape types," but with the novel contribution of binding signature types, which specify the bindings and scope of a macro’s arguments.

ACM Press Release:

The ACM Special Interest Group on Programming Languages (SIGPLAN) today presents its first-ever Programming Languages Software Award to Chris Lattner of Apple Inc. for his design and development of the Low Level Virtual Machine (LLVM), a compiler infrastructure that has been quickly adopted by a wide array of industry and academic organizations. Since LLVM’s release as an open source compiler infrastructure in October 2003, companies including Apple, Adobe, and Cray have incorporated it into their commercial products, reflecting its simplicity, flexibility, and versatility.

Racket is a programming language. Racket is the language implementation formerly known as PLT Scheme. Racket is available now. To quote the release announcement:

With Racket, you can script command shells and web servers; you can
quickly prototype animations and complex GUIs; regexps and threads
are here to serve you. To organize your systems, you can mix and
match classes, modules or components. Best of all, you start
without writing down types. If you later wish to turn your script
into a program, equip your Racket modules with explicit type
declarations as you wish. And Racket doesn't just come as a typed
variant; you can also write your modules in a purely functional and
lazy dialect.

Racket comes in so many flavors because Racket is much more than a
standard scripting language or a plain programming language. Racket
supports language extensibility to an unequaled degree. A Racket
programmer knows that making up a new language is as easy as writing
a new library.

If you haven't looked at, say, Typed Racket or how to create your own languages in Racket, now might be a good time.