Lambda the Ultimate

Seemingly a fair number of bugs in software stem from the complexity of the dynamic nature of runtime: concurrency issues, rare this-then-that-equals-infinite-loop issues, etc. How can a programming language be designed to try to make the static source more directly either reveal the runtime possibilities, or better constrain them to avoid confusion and thus bugs? Some languages do that by choosing better defaults (Erlang, Haskell, etc.) but obviously they don't constrain away all the differences between source and runtime. Presumably no language could, and still be all that useful. But how close could one usefully get?

Sure, having an IDE that generates UML interaction diagrams for all the possible concurrent API call interleavings might in some sense help, but tools along those lines really feel like mistakenly allowing grape juice in the room at all.

Since sundry tools for miscellaneous languages do already exist, I am more interested in how to refine/constrain core languages rather than ancillary tools. But, how could one at least provide tools to help e.g. automatic deadlock detection for CSP, or design-by-contract to effectively constrain the runtime state?

Let's suppose you have a language feature that only some code should have access to. For instance, Intensional Type Analysis/Reflection (ITA) can break abstraction barriers. Sometimes this sort of abstraction breaking is desirable, such as in generic pickling/serialization, printing, etc. but often it is not (violates parametricity theorems).

However, if we expose ITA as a language construct, then there are no restrictions on its use. So what we want is controlled abstraction breaking.

One solution is that ITA is exposed as a runtime provided object/module called Inspector. Inspector's signature has no constructor, so there is no way to construct an instance of it. Instead, an instance of Inspector is member of a standard set of such runtime objects that are provided to "main" and defines the "initial state of the world". "main" can then delegate access to Inspector to any code it deems should have it.

This is a capability design. However, I'm wondering if there's some way to express this constraint within the language itself, instead of resorting to a design pattern. In other words, keep ITA as a language construct, but somehow be able to express when it is legal to use ITA.

As an example of a possible solution, suppose we have a process language and two process constructors, one of which permits ITA expressions within it, the other of which doesn't:

expr  ::= process(expr) | lexpr | ita(expr)
lexpr ::= confined(lexpr) | ...

So a confined process cannot create an ordinary process or invoke ita. However, the composibility of the runtime Inspector object seems greater. Are there any other possibilities?

Modular Verification of Code with SAT (pdf)

"For this case study, we used a pre-existing specification of the Java List interface written in the Java Modeling Language (JML) ...
an approach to checking object-oriented code against detailed specifications that is fully automatic, demanding from the user only a specification of the method to be checked, an indication of the size of the space to be searched, and for each distinct representation, an abstraction function and representation invariant."

Using Alloy's Kodkod - a new relational engine designed to be a plugin component / backend for other tools. (It solves Sudoku too...)

Those of you who apply advanced PL ideas to operating systems might be interested in the upcoming PLOS 2007 workshop. See the abbreviated CFP below, and please consider submitting a short paper!

Thanks! ---

Eric.

Historically, operating system development and programming language development went hand-in-hand. Today, although the systems community at large retains an iron grip on C, many people continue to explore novel approaches to OS construction based on new programming language ideas. This workshop will bring together researchers and developers from the programming language and operating system domains to discuss recent work at the intersection of these fields. It will be a platform for discussing new visions, challenges, experiences, problems, and solutions arising from the application of advanced programming and software engineering concepts to operating systems construction, and vice versa.

Please visit the Web site for more info: http://plosworkshop.org/2007/

Looks like Chris Oliver's F3 has become openjfx, as of JavaOne. I'm slightly perturbed by Harold's casual dismissal of it...openjfx is integrating a dependency management system into the core of the language, and my gut is that it will be quite effective for the UI tasks it's targeted at. We really do need new thinking here, and new languages/syntax for it.

Lots to explore here, including a netbeans plugin.

So the question is...how effective is this UI-oriented DSL going to be? Is it more productive? Easier to use? And how can we quantify that?

RJ

(note: I guess I should add that Harold is rather famously stodgy when it comes to language change, and apparently even alternatives ;)

(notenote: I think F3 was a better name. Binding this language and technology to the Java brand on the desktop is a mistake. All that does is create confusion about what it is.)

From Type-Safe Casts by Stephanie Weirich

In a language with non-parametric or ad-hoc polymorphism,
it is possible to determine the identity of a type variable at
run time. With this facility, we can write a function to convert
a term from one abstract type to another, if the two
hidden types are identical. However, the naive implementation
of this function requires that the term be destructed and
rebuilt. In this paper, we show how to eliminate this overhead
using higher-order type abstraction. We demonstrate
this solution in two frameworks for ad-hoc polymorphism:
intensional type analysis and type classes.

This is a Functional Pearl, which was recommended in a previous discussion here.

So I'm looking at the pseudo-code example given:

sig
  type table
  val empty : table
  val insert : \forall 'a . table -> (string * 'a) -> table
  val find : \forall 'a . table -> string -> 'a
end

and I find myself wandering why not parameterize the table type (making it a kind).

Retaining pseudo-code:

sig
  kind table['t]
  val empty : table[nil]
  val insert : \forall 'a . \forall 'b . table['b] -> (string * 'a) -> table['b | 'a]]
  val find : \forall 'a . table['a] -> string -> 'a
end

As far as I know this is theoretically sound, or am I mistaken? I am still not comfortable with Haskell syntax so I was unable to decipher the rest of the paper. Any help would be appreciated.

Formalizing and extending C# type inference (pdf), Gavin Bierman

"Unfortunately this part of the published language specification is a little terse, and hence this feature can often behave in surprising ways for the programmer. Moreover, this process is quite different from the better known one implemented in Java 5.0. In this paper we attempt a formal reconstruction of the type inference process as it is currently implemented in C# 2.0."

Please join us for the next FringeDC informal meeting near the Eastern
Market in Washington DC for beer & talk about stuff (monadic
transformers, Amazon S3, delimited continuations- the typical kind of
stuff people chat about on a Saturday night)

FringeDC is a group for people interested in functional and lisp-like
languages. (Haskell, Erlang, Scheme, CL, etc) Anyone is welcome!

Main Site: www.lisperati.com/fringedc.html
Meeting Info: www.lisperati.com/may12th.html

Don Stewart has collected (all?) the Functional Pearls from JFP, ICFP, and elsewhere onto http://www.haskell.org/haskellwiki/Research_papers/Functional_pearls. Most of the are available online and are linked to from here. If you know what a Functional Pearl is, then you will enjoy this page, if not, you are in for a treat. Finally, if you know where any of the offline ones are publically available on the internet, that would be useful (just update the page).

Does anyone know if there is a point free translation of the pi calculus similar to using SK combinators to translate the Lambda calculus?

Specifically, I would like to express the Pi calculus in terms of combinators only (no mechanism for new variable names), and although I think I can do this with SK combinators plus a couple primitives, I am wondering if there is any existing work on this.