Lambda the Ultimate

[Edit: Previous LtU discussions. I guess I'm hoping to learn if there is anything new, new, new!]

Where might I find a language that infers static types (a la Haskell, SML, O'Caml) and yet also allows for late binding (a la Smalltalk, Lisp). I know some folks have tried to do it for Smalltalk and even for Lisp, but none are particularly 'main stream'. Are there any other obvious things I'm failing to recall?

Ah, the Merd page led me to soft typing! The dates on all the papers in Google hits look old. The only thing that appears to still be kicking is PLT's Mr. Spidey debugger. Has anybody had experience with it, per chance?

Found this linked in the comments section of an interview with Charles Simonyi

http://www.cse.unsw.edu.au/~cs3141/ip.asf

While some researchers seek to generalize monads (to arrows), others try to narrow the focus to achieve a richer theory (and probably deeper understanding).

Combining computational effects: commutativity and sum

We begin to develop a unified account of modularity for computational effects. We use the notion of enriched Lawvere theory, together with its relationship with strong monads, to reformulate Moggi's paradigm for modelling computational effects; we emphasise the importance here of the operations that induce computational effects. Effects qua theories are then combined by appropriate bifunctors (on the category of theories). We give a theory of the commutative combination of effects, which in particular yields Moggi's side-effects monad transformer (an application is the combination of side-effects with nondeterminism). And we give a theory for the sum of computational effects, which in particular yields Moggi's exceptions monad transformer (an application is the combination of exceptions with other effects).

(Via the JML list.) The docs are skimpy, but they claim to extend "environments with type systems, which provide an automated means to enforce many basic policies, and use the resulting framework to cover a wide range of security policies for global computers."

Through their global, uniform provision of services, and their distributed nature, global computers have the potential to profoundly enhance our daily life. However, they will not realize their full potential, unless the necessary levels of trust and security can be guaranteed.

We aim to develop the technology for establishing trust and security for the next generation of global computers, using the Proof Carrying Code (PCC) paradigm.

The Anatomy of a Loop by Olin Shivers

…the lexical-scope rule of the classic λ-calculus, which we’ll call “LC scope,” implies an important property: it ensures that binders dominate references. The key design idea that serves as the foundation for our extensible loop form is to invert cause and effect, taking the desired property as our definition of scope. This gives us a new scoping rule, which we call “BDR scope.”

From this concept, Shivers builds a sub-language for describing iterations which includes what is effectively a directed graph of scopes, rather than a simple tree. Parallel code paths (or perhaps a better description would be unordered code paths) can independently contribute to the binding scope of following code, without being visible to each other. (See the example of quicksort on page 11.)

Is this too wierd for real programmers? Or is it a stunningly elegant way of capturing something important about parallel code flows? I vote for the second but I wonder what other LtUers think