Lambda the Ultimate

As part of the ongoing design of the ParaSail programming language, we settled on a "pointer free" approach. Given that pointers (or references in Java parlance) are rather fundamental to almost all modern languages which allow the user definition of structures like trees, lists, sets, maps, graphs, etc., this seems like a risky decision. In fact, we have been very pleased with the result, and in some ways it requires only a slight shift from the familiar programming model, while in other ways it makes for a dramatic simplification in storage management, assignment semantics, analyzability, etc.

Coupled with a few other ParaSail rules, the elimination of pointers makes it as easy to parallelize ParaSail as it is to parallelize a pure side-effect-free functional language, while remaining very much in the familiar territory of the Java/C# class-and-interface-based object-oriented programming world. Overall, ParaSail is a pleasure to program in, and this is in no small part due to the elimination of pointers from the surface syntax and semantics of the language. Of course, pointers are likely to still be used behind the scenes by any ParaSail implementation, but that doesn't affect the simplicity provided at the programmer level of having banished them.

We have written a longer "blog" entry on this topic here:

http://parasail-programming-language.blogspot.com/2012/08/a-pointer-free-path-to-object-oriented.html

The Economist Language blog just posted an essay on the differences between computer code and natural language, taking a negative stance on their relationship. For all the talk of grammar, perhaps the title should have been "Why computer code isn't language".

Some of the qualities said to not exist in PL could be argued the other way ("dialects, idiolects, variation, natural change over time"). Additionally, though PL do not typically have some qualities mentioned, PL could and have been constructed to have some of these qualities mentioned in the article. Am I in the minority for thinking different than than article?

It is easy to find questionable aspects of the javascript language, but there is at least one feature that it gets right: the composable concurrency model. The built in event loop and the continuation passing style allows completely different IO stacks, or many instances of the same stack to be easily composed in nodejs. Since every IO is asynchronous, the javascript programmer is forced to do the hard work and write code that fires as much asynchronous IO operation concurrently as possible, and to join the results in callbacks. This is not possible in a threaded programming language, since that encourages the programmer to write serial code, and the same holds if you use monads in Haskell which serializes all calls for you.

Here is an example application: suppose you want to traverse a large tree (directory structure or tree stored in a database) and print it out in a depth first fashion (or as an XML file with embedded child objects). If you use monads, then you will issue IO operations sequentially: first get the directory of the root, then the directory of the first child, then the directory of the first child of the first child, etc. However, the IO operations are slow, so you want to fire them concurrently. If you do this blindly, then you effectively do breadth first search as you issue IO operations, but then you have to store the results in memory to print it out in depth first, which will explode the memory overhead. Clearly, the best is some combination (use depth first search to drive the traversal, but at any point you issue extra queries that are expected to come soon).

Is it possible to write this depth first search concurrently in Haskell? The best would be to have a "handle" for file IO, or for socket IO, which you can use to serialize IO operations when necessary and execute IO parallel when necessary. I would like to execute operations A and B concurrently, but force the console IO to be serialized, however allow e.g. read only file IO to be parallel. I do not want to solve this problem by serializing the execution of A and B, only their console IO needs to be serialized. Is this possible?

The following article describes a verified version of the heapsort algorithm.

The verified heapsort algorithm is another example on how ghost functions/predicates can be used to describe loop invariants in a exact and concise manner.

At the day job I have an API in which part of it has a structure like so (in pseudo code):


function NewStyleHandle(doc : Document, style : Style) : StyleHandle
function AddContent(doc : Document, content : Text, styling : StyleHandle) : Void


The problem we've run into is that this mistake is pretty easy to make:

declare a : Document
declare b : Document
declare s : Style
declare c : Text

AddContent(a, c, NewStyleHandle(b, s))


The "StyleHandle"s have a sort of scope in the document they're created by. Use the wrong one, and at runtime "bad things" happen. I can check this at runtime, but by then it's too late to alert the programmer, and any default action I take will still be incorrect. I can change the interface, and have AddContent take a Style instead of a StyleHandle, but if you'd be so kind humor me and assume that's off the table.

One approach that has occurred to me is to use witness types, like Document a and StyleHandle a. I believe that could solve the problem, or at least reduce the likelihood of it, but it requires the end user to whip up a new witness type for every instance of document, and the constraint presented by the API isn't quite the one I want to express.

It seems like regions might be applicable, but I don't really need to manage the lifetime of the handles as such, just be sure that they don't get mixed up. Am I barking up the wrong tree? Should I be looking at dependent types? I don't necessarily expect to be able to actually apply a solution like this (although the type witness would be workable, for some definitions thereof), but it would be nice to be able to say "and that's how you prevent this statically" for my own satisfaction if nothing else.

I wonder if there are any strategies for overloading by a type of a return value in dynamically types languages. There is one example I am aware about - Perl and its "contexts". May be there are some other insights on this topic?

Basically I mean run-time dispatch on the return values so that the code like so:

//This function is overloaded for int32
maxValue _ = 0x7fffffff

x = maxValue 0

can be translated into

//Overloaded (polymorphic) constant
maxValue = 0x7fffffff

x = maxValue ::: Int

without the need to statically type the program.

Somewhat to my surprise, I may have found a politically acceptable way to extend C in a way that leads to the prevention of buffer overflows. Many people have struggled with this, but the previous attempts led to incompatibility, excessive overhead, or a new language.

It turns out that combining C fixed size arrays, C++ references, and C99 variable-length automatic arrays seems to lead to a workable solution. An example is declaring the UNIX read call in this way:

Present C form of declaration:
int read(int fd, char* buf, size_t n);
Proposed form:
int read(int fd, char (&buf)[n], size_t n);
This is size-safe when called from new code, compatible with old code, and type-checkable at calls.

There's more, of course; see the draft paper: "Safe Arrays and Pointers for C" (PDF)

Now I need to find out if someone can find a flaw in this, so it needs to go before a qualified critical audience. So I'd like to see what the LtU crowd has to say about this. Thanks.

An Executable Formal Semantics of C with Applications
Chucky Ellison & Grigore Rosu, POPL '12

This paper describes an executable formal semantics of C. Being executable, the semantics has been thoroughly tested against the GCC torture test suite and successfully passes 99.2% of 776 test programs. It is the most complete and thoroughly tested formal definition of C to date. The semantics yields an interpreter, debugger, state space search tool, and model checker “for free”. The semantics is shown capable of automatically finding program errors, both statically and at runtime. It is also used to enumerate nondeterministic behavior.

This is the most ambitious use of rewriting logic that I've yet seen. On its face it seems like a quite elegant and general-purpose formulation; this specific C semantics is open sourced, even.

For more background I recommend the main page on the K framework.

Anyone else investigating this system and style of semantics definition?

It appears that the Fortress project is wrapping up. I'd be interested in seeing more commentary of lessons learned.

I originally posted a proposed definitions and rationale about a week ago. But I've revised them based on feedback and I think I'm ready for the PL community to review the proposal.

An object is a first-class, dynamically dispatched behavior. A behavior is a collection of named operations that can be invoked by clients where the operations may share additional hidden details. Dynamic dispatch means that different objects can implement the same operation name(s) in different ways, so the specific operation to be invoked must come from the object identified in the client's request. First class means that objects have the same capabilities as other kinds of values, including being passed to operations or returned as the result of an operation.

A language or system is object oriented if it supports the dynamic creation and use of objects. Support means that objects are easy to define and use. It is possible to encode objects in C or Haskell, but an encoding is not support.