Virgil: a statically-typed language balancing functional and OO features

In PLDI this year: Ben Titzer, "Harmonizing Classes, Functions, Tuples, and Type Parameters in Virgil III" [pdf]

Given a fresh start, a new language designer is faced with a daunting array of potential features. Where to start? What is important to get right first, and what can be added later? What features must work together, and what features are orthogonal? We report on our experience with Virgil III, a practical language with a careful balance of classes, functions, tuples and type parameters. Virgil intentionally lacks many advanced features, yet we find its core feature set enables new species of design patterns that bridge multiple paradigms and emulate features not directly supported such as interfaces, abstract data types, ad hoc polymorphism, and variant types. Surprisingly, we find variance for function types and tuple types often replaces the need for other kinds of type variance when libraries are designed in a more functional style.

It's Alive! Continuous Feedback in UI Programming

A paper by Burckhardt et al that will appear at PLDI 2013. Abstract:

Live programming allows programmers to edit the code of a running program and immediately see the effect of the code changes. This tightening of the traditional edit-compile-run cycle reduces the cognitive gap between program code and behavior, improving the learning experience of beginning programmers while boosting the productivity of seasoned ones. Unfortunately, live programming is difficult to realize in practice as imperative languages lack well-defined abstraction boundaries that make live programming responsive or its feedback comprehensible.

This paper enables live programming for user interface programming by cleanly separating the rendering and non-rendering aspects of a UI program, allowing the display to be refreshed on a code change without restarting the program. A type and effect system formalizes this separation and provides an evaluation model that incorporates the code update step. By putting live programming on a more formal footing, we hope to enable critical and technical discussion of live programming systems.

DYNAMO

I was surprised to see that DYNAMO hasn't been mentioned here in the past. DYNAMO (DYNAmic MOdels) was the simulation language used to code the simulations that led to the famous 1972 book The Limits to Growth from The Club of Rome. The language was designed in the late 1950s. It is clear that the language was used in several other places and evolved through several iterations, though I am not sure how extensively it was used. When Stafford Beer was creating Cybersyn for Salvador Allende he used DYNAMO to save time suggesting it was somewhat of a standard tool (this is described in Andrew Pickering's important book The Cybernetic Brain).

The language itself is essentially what you'd expect. It is declarative, programs consisting of a set of equations. The equations are zero and first-order difference equations of two kinds: level equations (accumulations) and rate equations (flows). Computation is integration over time. Levels can depend on rates and vice versa with the language automatically handling dependencies and circularities. Code looks like code looked those days: fixed columns, all caps, eight characters identifiers.

Here are a few links:

  • Section 3.7 of this history of discrete event simulation languages is a succinct description of the history of the language and its main features.
  • A more leisurely description of the language and the Limits to Growth model can be found in this article. Ironically, the author of the article reimplemented the model in Javascript (run it!). What was originally written in a DSL is now implemented in a general purpose language, with all the niceties handled manually.
  • Finally, a nice piece on Jay Forrester who prompted the creation of SIMPLE and DYNAMO, its offspring.

LtU is migrating from Drupal

As many of you know we have been suffering for a long time from the deficiencies of Drupal. We have not updated our infrastructure for a long time. Among the features members have been asking for are better integration with other sites and more social features. In particular, many said they want to be able to mark the posts that they find particularly helpful. I am happy to announce that we have big news!

In the coming days we will be migrating LtU from Drupal to Facebook. All the awesome features of Facebook will be automatically available; in particular the "Like" mechanism. You will also be able to share photos with other PLT enthusiasts, re-share their shares etc. Best of all, you will be guaranteed the privacy standards of Facebook.

Rest assured, we have not made this decision without considering the alternatives. We studied Google+ but given Google's unprovoked assault on RSS with the decision to discontinue Google Reader we found it unconscionable to go with Google.

LtU's twitter feed will have to go, I am afraid, given the relationship between our new home and twitter. Hopefully this issue will be resolved once twitter gives up and is acquired by FB.

The LtU feed will have ads, per usual on FB. I know this is somewhat of an inconvenience, but at least the ads you will be served will be personalized[1].

Ehud and the LtU Team.

[1] I am assured that ads for dynamically typed and scripting languages will never be served to you again after you mark them as "offensive" once.


Update: No, we are not migrating to Facebook. This was an April Fools joke.

Who's online

Earlier today I enabled a drupal feature that list the names of users currently online. It was on the bottom of the right-hand navigation bar, and looked something like this:

Who's online
There are currently 7 users and 887 guests online.
Online users:

Matt M
Ehud Lamm
Mattias Engdegård
naasking
Andreas Rossberg
...

Some might see this as a privacy violation or otherwise object. Since I heard complaints I disabled this feature. What do you think?

What is the most bizarre thing you have seen done with TeX?

Dependent Types for JavaScript

Dependent Types for JavaScript, by Ravi Chugh, David Herman, Ranjit Jhala:

We present Dependent JavaScript (DJS), a statically-typed dialect of the imperative, object-oriented, dynamic language. DJS supports the particularly challenging features such as run-time type-tests, higher-order functions, extensible objects, prototype inheritance, and arrays through a combination of nested refinement types, strong updates to the heap, and heap unrolling to precisely track prototype hierarchies. With our implementation of DJS, we demonstrate that the type system is expressive enough to reason about a variety of tricky idioms found in small examples drawn from several sources, including the popular book JavaScript: The Good Parts and the SunSpider benchmark suite.

Some good progress on inferring types for a very dynamic language. Explicit type declarations are placed in comments that start with "/*:".

/*: x∶Top → {ν ∣ite Num(x) Num(ν) Bool(ν)} */
function negate(x) {
    if (typeof x == "number") { return 0 - x; }
    else { return !x; }
}

Concurrent Revisions

Concurrent Revisions is a Microsoft Research project doing interesting work in making concurrent programming scalable and easier to reason about. These papers work have been mentioned a number of times here on LtU, but none of them seem to have been officially posted as stories.

Concurrent Revisions are a distributed version control-like abstraction [1] for concurrently mutable state that requires clients to specify merge functions that make fork-join deterministic, and so make concurrent programs inherently composable. The library provide default merge behaviour for various familiar objects like numbers and lists, and it seems somewhat straightforward to provide a merge function for many other object types.

They've also extended the work to seamlessly integrate incremental and parallel computation [2] in a fairly intuitive fashion, in my opinion.

Their latest work [3] extends these concurrent revisions to distributed scenarios with disconnected operations, which operate much like distributed version control works with source code, with guarantees of eventual consistency.

All in all, a very promising approach, and deserving of wider coverage.

[1] Sebastian Burckhardt and Daan Leijen, Semantics of Concurrent Revisions, in European Symposium on Programming (ESOP'11), Springer Verlag, Saarbrucken, Germany, March 2011
[2] Sebastian Burckhardt, Daan Leijen, Caitlin Sadowski, Jaeheon Yi, and Thomas Ball, Two for the Price of One: A Model for Parallel and Incremental Computation, in Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'11), ACM SIGPLAN, Portland, Oregon, 22 October 2011
[3] Sebastian Burckhardt, Manuel Fahndrich, Daan Leijen, and Benjamin P. Wood, Cloud Types for Eventual Consistency, in Proceedings of the 26th European Conference on Object-Oriented Programming (ECOOP), Springer, 15 June 2012

Feature-Oriented Programming with Object Algebras

Feature-Oriented Programming with Object Algebras, by Bruno C.d.S. Oliveira, Tijs van der Storm, Alex Loh, William R. Cook:

Object algebras are a new programming technique that enables a simple solution to basic extensibility and modularity issues in programming languages. While object algebras excel at defining modular features, the composition mechanisms for object algebras (and features) are still cumbersome and limited in expressiveness. In this paper we leverage two well-studied type system features, intersection types and type-constructor polymorphism, to provide object algebras with expressive and practical composition mechanisms. Intersection types are used for defining expressive run-time composition operators (combinators) that produce objects with multiple (feature) interfaces. Type-constructor polymorphism enables generic interfaces for the various object algebra combinators. Such generic interfaces can be used as a type-safe front end for a generic implementation of the combinators based on reflection. Additionally, we also provide a modular mechanism to allow different forms of self-references in the presence of delegation-based combinators. The result is an expressive, type-safe, dynamic, delegation-based composition technique for object algebras, implemented in Scala, which effectively enables a form of Feature-Oriented Programming using object algebras.

A follow-up to Object Algebras, this new paper addresses a few of the limitations described in that LtU thread by adding type constructor polymorphism to increase their safety. The paper describes an implementation in Scala, which is the only widely available statically typed OOP language with a sufficiently powerful type system needed to support FOP.

This new work also describes some composition mechanisms for object algebras in the context of more expressive languages.

Twenty Reasons Why You Should Use Boxer (Instead of LOGO)

An old paper on boxer that I found while reviewing related work for a paper I'm writing, abstract:

Boxer was designed as a successor to Logo, with the same educational goals in mind. Whereas Logo has incrementally added features over the years, Boxer changes the
core computational structures of the language and environment. The aim is to make
learning easier and more rewarding, especially over the long term.

As an early graphical language, it is quite interesting. It is one of the first works I know of that dive into concreteness (they call naive realism):

Here, the idea is that the user of a computer system can pretend that what appears on the screen is the computer system. That is, you don’t need to do a lot of mental work interpreting an abstract presentation that relates only indirectly to the fact of the matter (as, for example, imagining something called a variable that is changed or accessed by commands). Instead, naive realism means that everything in the system must have a visual presentation that allows easy interaction with it, including creating it, changing it, moving it, and deleting it.

As well as one of the first languages to use spatial relationships in programming (the only other I know being...agent sheets):

Boxer uses space and spatial relations systematically to represent aspects of “abstract” computation. In particular, Boxer has a wonderfully transparent hierarchical structure of boxes inside of boxes that represents huge ranges of computational meanings.

But what I really like is this notion of pokability:

Logo has always, unfortunately, distinguished in one way or another the mode of creating procedures from the mode of executing them...you cannot easily—or at all!—see the effects of a procedure at the same time that you look at its form. This makes learning by inspecting difficult; you have to flip back and forth between different areas to see a procedure and its effects. In addition, it rules out a mode of learning by interacting with pieces of code, which is very powerful and characteristic of Boxer. For example, if you look at a line of code in Boxer and wonder what it will do, you can just double-click on that line, and it will be executed. This also turns out to be an extremely powerful debugging technique. If something goes wrong, you can just step through the process by executing one line at a time. That is, the inherent inspectabiliy of Boxer is extended with “pokability.”

And so on....