Lambda the Ultimate

Most of you have probably heard about Microsoft's now-completed Visual Studio 2020 competition, where the grand prize was to meet Scott Guthrie, the effective head of the Developer Division. People were invited to make submissions, and one of them was shown on Code Project and began life as the Visual Studio 2010 Concept IDE.

Well, Ph.D. student Andrew Bragdon has his own take on "inventing the future". Code Bubbles is an IDE that will be presented at this years ICSE. The level of thought that has gone into this design is simply astonishing. It has the feel of a tiling window manager like XMonad or awesomewm, but without the traditional MDI Application or SDI Application WIMP metaphors we're used to; as a result, it eliminates a ton of clutter. It also integrates key ideas from Eclipse contributed by Mik Kersten and Borland/CodeGear: The Mylyn project for integrating workflow deeply into the IDE. This is some real inspiration for Gilad Braha's Newspeak project (Vassili Bykov's Hopscotch IDE; LANG.NET 2009) and Dan Ingalls' Lively Kernel, since the staple of any good Smalltalk-like language is the environment!

Will makers of 30" monitors will be shaking developers down by their ankles? :)

I've been watching the interpreter and JIT compiler competitions a bit in the JavaScript and Lua worlds. I haven't collected much organized data but the impression I'm getting is that tracing JIT's are turning up as the winners: sometimes even beating programs statically compiled with GCC. Is there a growing body of evidence that tracing JIT compilers are the horse to bet on? Will a more static style JIT like Google's V8 be able to keep up?

Thanks,
Peter

[I promoted this item to the front page, since the discussion is highly interesting & informative. -- Ehud]

Extending the Scope of Syntactic Abstraction by Oscar Waddell and R. Kent Dybvig, POPL '99. (Also: Waddell's thesis with the same title.)

The benefits of module systems and lexically scoped syntactic abstraction (macro) facilities are well-established in the literature. This paper presents a system that seamlessly integrates modules and lexically scoped macros. The system is fully static, permits mutually recursive modules, and supports separate compilation. We show that more dynamic module facilities are easily implemented at the source level in the extended language supported by the system.

This paper is probably known to many LtUers, but it's never been posted, and I find it very enjoyable.

It introduces two very simple forms, (module name exports-list body) for naming and enclosing a body of code containing definitions and expressions, and (import module-name) for importing the definitions from such a module into the current scope.

Module names are lexically scoped just like variables, and modules can appear wherever definitions can occur, so one can define modules (say) inside a lambda. Furthermore, modules and import forms may also be generated by macros.

They show how more advanced features (such as qualified references ("module::var"), anonymous modules, selective importing and renaming, and mutually recursive modules, among others) can be built on top of this simple base using a hygienic macro system, cleverly and without much fuss.

Side note: such a "syntactic" module system can be contrasted with R6RS's "static" library system. There is currently some discussion to this effect in the Scheme community.

From the title Can a Biologist Fix a Radio? — or, What I Learned while Studying Apoptosis(Y. Lazebnik 2004) would seem pretty off topic for LtU. It starts with a humorous take on how biologist might try to understand the workings of a radio, but it ends in a plea for (computer aided) formal languages and quantitative modeling of biological systems.

The question is how to facilitate this change, which is not exactly welcomed by many experimental biologists, to put it mildly. Learning computer programming was greatly facilitated by BASIC, a language that was not very useful to solve complex problems, but was very efficient in making one comfortable with using a computer language and demonstrating its analytical power. Similarly, a simple language that experimental scientists can use to introduce themselves to formal descriptions of biological processes would be very helpful in overcoming a fear of long forgotten mathematical symbols. Several such languages have been suggested but they are not quantitative, which limits their value. Others are designed with modeling in mind but are too new to judge as to whether they are user friendly. However, I hope that it is only a question of time before a user friendly and flexible formal language will be taught to biology students, as it is taught to engineers, as a basic requirement for their future studies. My advice to experimental biologists is to be prepared.

Further, at a meta-level, the issues he raises seem to directly mirror the challenges software developers and researchers face in trying to understand and design complex computing systems. If nothing else it's good to know we're not alone.

And it doesn't hurt at all that it's a fun read.

Objects to Unify Type Classes and GADTs, by Bruno C. d. S. Oliveira and Martin Sulzmann:

We propose an Haskell-like language with the goal of unifying type classes and generalized algebraic datatypes (GADTs) into a single class construct. We treat classes as first-class types and we use objects (instead of type class instances and data constructors) to define the values of those classes. We recover the ability to define functions by pattern matching by using sealed classes. The resulting language is simple and intuitive and it can be used to define, with similar convenience, the same programs that we would define in Haskell. Furthermore, unlike Haskell, dictionaries (or
objects) can be explicitly (as well as implicitly) passed to functions and we can program in a simple object-oriented style directly.

A very interesting paper on generalizing and unifying type classes and GADTs. Classes are now first-class values, resulting in a language that resembles a traditional, albeit more elegant, object-oriented language, and which supports a form of first-class "lightweight modules".

The language supports the traditional use of implicit type class dispatch, but also supports explicit dispatch, unlike Haskell. The authors suggest this could eliminate much of the duplication in the Haskell standard library of functions that take a type class or an explicit function, eg. insert/insertBy and sort/sortBy, although some syntactic sugar is needed to make this more concise.

Classes are open to extension by default, although a class can also be explicitly specified as "sealed", in which case extension is forbidden and you can pattern match on the cases. Furthermore, GADTs can now also carry methods, thus introducing dispatch to algebraic types. This fusion does not itself solve the expression problem, though it does ease the burden through the first-class support of both types of extension. You can see the Scala influences here.

I found this paper via the Haskell sub-reddit, which also links to a set of slides. The authors acknowledge Scala as an influence, and as future work, suggest extensions like type families and to support more module-like features, such as nesting and opaque types.

I'd like to announce the public debut of a service I've been working on. Among other things, it provides "cloud hosting" for web applications written in Ur/Web, a domain-specific functional language for "Web 2.0 programming."

http://www.graftid.com/

This service (called Graftid) also enables communities of developers to work together to build tools that non-programmers can use to build customized web sites quickly. Anyone can upload a site-generator GUI, which is implemented in Ur/Web and also generates Ur/Web code, based on what a user enters into the GUI. Everything is statically-typed, and it's possible to use combinators to minimize the cost of building a new GUI. Every GUI inherits a platform for automatic deployment of applications, without the need to write a line of code that has a server-side side effect.

I'm looking for curious folks who might like to put this platform through its paces, finding bugs, security-oriented and otherwise. I hope that many LtU readers will find this a very pleasant platform for building buzzword-compliant web apps, without the need to learn much about the buzzwords and their associated technologies. :)

I also have a related question that I thought I'd include with this post: We're all used to encapsulation for examples like data structures: a class or module "owns" a representation, and the representation may only be accessed by going through the class or module's published interface. Ur/Web extends this facility to let you code a module that owns a cookie, a database table, a subtree of the client-side DOM for a particular page rendering, etc.. Think "Facebook apps" with static enforcement of which app may touch which resource, but without the need for any dynamic enforcement, and with the possibility for running all the apps on the same server; we just combine first-class web app pieces with standard encapsulation techniques. Does anyone know of any other systems that allow this? Has the desirability of this facility been articulated somewhere?

The call for papers for the SPLASH conference is now up.

SPLASH is the conference formerly known as OOPLSA, and the OOPSLA name is now being used for one of the two main colocated events at SPLASH (the other being Onward!). So if you've got a paper full of interesting results, send it in by March 25.

EDIT: both Martin Rinard in the comments below, and William Cook in email, have been very emphatic that the name change is to make clear that the conference is not just about objects any more -- anything that's (a) about programming languages maximally broadly construed, and (b) good work, is fair game for the conference now. Sorry for any confusion!

A Lambda Calculus for Real Analysis

Abstract Stone Duality is a revolutionary paradigm for general topology that describes computable continuous functions directly, without using set theory, infinitary lattice theory or a prior theory of discrete computation. Every expression in the calculus denotes both a continuous function and a program, and the reasoning looks remarkably like a sanitised form of that in classical topology. This is an introduction to ASD for the general mathematician, with application to elementary real analysis.

This language is applied to the Intermediate Value Theorem: the solution of equations for continuous functions on the real line. As is well known from both numerical and constructive considerations, the equation cannot be solved if the function "hovers" near 0, whilst tangential solutions will never be found.

In ASD, both of these failures and the general method of finding solutions of the equation when they exist are explained by the new concept of overtness. The zeroes are captured, not as a set, but by higher-type modal operators. Unlike the Brouwer degree, these are defined and (Scott) continuous across singularities of a parametric equation.

Expressing topology in terms of continuous functions rather than sets of points leads to treatments of open and closed concepts that are very closely lattice- (or de Morgan-) dual, without the double negations that are found in intuitionistic approaches. In this, the dual of compactness is overtness. Whereas meets and joins in locale theory are asymmetrically finite and infinite, they have overt and compact indices in ASD.

Overtness replaces metrical properties such as total boundedness, and cardinality conditions such as having a countable dense subset. It is also related to locatedness in constructive analysis and recursive enumerability in recursion theory.

Paul Taylor is deadly serious about the intersection of logic, mathematics, and computation. I came across this after beating my head against Probability Theory: The Logic of Science and Axiomatic Theory of Economics over the weekend, realizing that my math just wasn't up to the tasks, and doing a Google search for "constructive real analysis." "Real analysis" because it was obvious that that was what both of the aforementioned texts were relying on; "constructive" because I'd really like to develop proofs in Coq/extract working code from them. This paper was on the second page of results. Paul's name was familiar (and not just because I share it with him); he translated Jean-Yves Girard's regrettably out-of-print Proofs and Types to English and maintains a very popular set of tools for typesetting commutative diagrams using LaTeX.

We present Joe-E, a language designed to support the development of secure software systems. Joe-E is a subset of Java that makes it easier to architect and implement programs with strong security properties that can be checked during a security review. It enables programmers to apply the principle of least privilege to their programs; implement application-specific reference monitors that cannot be bypassed; introduce and use domain-specific security abstractions; safely execute and interact with untrusted code; and build secure, extensible systems. Joe-E demonstrates how it is possible to achieve the strong security properties of an object-capability language while retaining the features and feel of a mainstream object-oriented language...

Section 5.2 discuss how Joe-E leverages Java static typing. Joe-E is implemented as a source-code verifier not a bytecode verifier. Section 6 of the paper explains this design choice.

Joe-E was mentioned on LtU in the past and is available here.

Quantum theory has acquired a reputation as an impenetrable theory accessible only after acquiring a significant theoretical physics background. One of the lessons of quantum computing is that this is not necessarily true: quantum computing can be learned without mastering vast amounts of physics, but instead by learning a few simple differences between quantum and classical information.

A well written article in the CACM.

There's also slides for a talk by Rob Pike on the same topic.