Lambda the Ultimate

There's a neat thread about strong normalization happening on The Types Forum.

If you've ever wondered Why is it useful to have {type systems,reductions,operations,...} that always terminate? this may Illuminate you.
Here are some snippets to give you a feel for the discussion:

I think it is clearer to split Gérard's original question in two:

1. Is strong normalization useful for programming languages ?
2. Is the proof of strong normalization via type systems applicable for programming languages?

-- François-Régis Sinot

Termination is good:

If a program is a solution to a problem then knowing that it terminates
for any input is an important aspect of it being a solution. Often the
best way to see that it is terminating is expressing it in a language
where all programs terminate. The programming language Epigram is an
example of an experimental language which is intended to be terminating
(even though not all conditions are enforced in the current version), see
http://www.e-pig.org/ for more information.

-- Thorsten Altenkirch

Termination is good!

I think the moral sense of strong normalization is that a program
in a strictly-typed language can only diverge as a result of some
programming construct, which _explicitly_ permits looping, like
iteration, recursion etc. My favourite example here is that the
"big Omega" can be written in Algol 60, because procedure types
in this language are not fully specified.

-- Pawel Urzyczyn

Termination is good and with fixpoints is turing complete?

Another way to put this is that data structures should be definable in a
strongly-normalising language so that data access, etc. is guaranteed to
terminate. Then add fixpoints or loops to describe arbitrary computations.

-- Barry Jay

Terminating reductions allows exhaustive applications of optimizations:

In a compiler, if a set of reductions is strongly normalizing, then the compiler can apply them exhaustively to an intermediate-language term without fear of looping. (We rely on this in the MLj and SML.NET compilers' "simplify" compilation phases, which apply simple reductions and directed commuting conversions until a normal form is reached. Though it has to be said that it's not the classical SN results that are relevant here, but something more specific to our intermediate language and the simplifying reductions that we employ).

-- Andrew Kenney

Rene Vestergaard also gave a link to a 2004 discussion of strong normalization on the rewriting list.

The Fortress specs have been updated.

http://research.sun.com/projects/plrg/fortress0785.pdf

X10 is a type-safe, modern, parallel, distributed object-oriented language intended to be very easily accessible to Java(TM) programmers. It is targeted to future low-end and high-end systems with nodes that are built out of multi-core SMP chips with non-uniform memory hierarchies, and interconnected in scalable cluster configurations. A member of the Partitioned Global Address Space (PGAS) family of languages, X10 highlights the explicit reification of locality in the form of places; lightweight activities embodied in async, future, foreach, and ateach constructs; constructs for termination detection (finish) and phased computation (clocks); the use of lock-free synchronization (atomic blocks); and the manipulation of global arrays and data structures.

X10 was mentioned here a couple of times, but I don't think it was ever discussed at length.

Here's the (relatively empty) IBM Research X10 home page.

Chris Adamson at OnJava.com published interviews with a few language luminaries and Java developers. Inspired by Bruce Tate's book Beyond Java, Adamson argues that Ruby is poised to become Java's successor:

Bruce Tate's Beyond Java argues that Java's reign as the top enterprise development language must eventually come to an end and that, for the first time in a decade, major enterprise innovation is occurring outside of the Java realm. In the book, he looks at the unique traits that has allowed to Java to achieve its unprecedented level of success, and then considers what new languages would have to do and be to succeed Java.

Later chapters look at specific languages contending in this space, and clearly favors Ruby as the front-runner. This comes from Tate's own performance breakthroughs (fueled by Ruby on Rails), an analysis of the language, and anecdotal evidence from others who've tried the language.

Is Ruby already shaping up to succeed Java? What's broken with Java that Ruby fixes? And are the two mutually incompatible?

To survey the situation, we contacted several prominent authors, bloggers, and developers to get their takes. Their responses are reprinted in whole in this article.

The interviews are a very interesting read, and the dialogue covers a diverse range of topics. The power of Ruby on Rails is a common theme throughout, and Tate argues that Rails is the catalyst that will push Ruby into the mainstream. What I don't understand is this: if Rails will make Ruby the next Java, why didn't Zope do that for Python?