Lambda the Ultimate

Didn't notice this being mentioned on LtU yet: PLT is going really really un-mutable, which seems like a rather cool and worthy experiment to my mind, and will probably highlight some of the more pragmatic and cultural aspects of managing the development of a language in light of the user community.

For PLT Scheme v4.0, we’re going to try it. In our main dialects of Scheme (such as the mzscheme language), cons will create immutable pairs, and pair? and list? will recognize only immutable pairs and lists. The set-car! and set-cdr procedures will not exist. A new set of procedure mcons, mcar, mcdr, set-mcar!, and set-mcdr! will support mutable pairs.

On page 56 at the top of the page he has the reduction:

( λx . x ( λx . x ) )( u r ) evaluates to u r ( λx . x )

My question is:

I see how the lhs can be written as: (id(id))(ur) which is then (id)(ur). What I don't get is: (id)(ur) = (ur)(id). Is the point that the identity term is commutative in this context? Is this the same idea as the composition operation between functions in that the composition of two functions is generally not commutative, but the identity function is always commutative?

Abstract: Array theory combines APL with set theory, transfinite arithmetic, and operationally transformed functions to produce an axiomatic theory in which the theorems hold for all arrays having any finite number of axes of arbitrary countable ordinal lengths. The items of an array are again arrays. The treatment of ordinal numbers and letters is similar to Quine's treatment of individuals in set theory. The theory is developed first as a theory of lists. This paper relates the theory to the eight axioms of Zermelo-Fraenkel set theory, describes the structure of arrays, interprets empty arrays in terms of vector spaces, presents a system of axioms for certain properties of operations related to the APL function of reshaping, deduces a few hundred theorems and corollaries, develops an algebra for determining the behavior of operations applied to empty arrays, begins the axiomatic development of a replacement operator, and provides an informal account of unions. Cartesian products, Cartesian arrays, and outer, positional, separation, and reduction transforms.

Preamble: The intention of the work reported here is to develop a theory of arrays, in terms of standard set theory, that will provide rigorous definitions for programming operations and thereby a logical foundation for the construction of programming languages. The present contribution is a first approach to establishing a comprehensive theory of arrays, and it is anticipated that future papers will extend and refine the concepts presented.

The objects used in programming are represented in a mathematical system of ordered collections as arrays of arrays. Simple axioms define certain primitive operations on the arrays. Most data operations in programming can then be represented by operations built upon the axioms. One of the starting points for the development of the theory is APL. Programs written in APL are used to generate corollaries of the axioms and to check the consistency of the system.

Although the paper was written for the specialist in mathematical logic, it should be of interest to the computer scientist and particularly to one who specializes in programming languages. Its chief contribution is an axiomatic theory for data structures, which includes explicit rules for transforming any operation into a new operation that applies to all items in any array.

I want to start making a compiler for a little programming language that I have in mind. I think that doing it right would teach me lot of new things. I want to target the JVM's bytecode using Jasmin or Jamaica but I want to know your opinions...

Is there another good choice to generate bytecode from the opcodes for the JVM?

What about other VM's? CLR is not as portable as JVM... I used Parrot once but i didnt like it in that time. Do you know other options?