Lambda the Ultimate

I'll start with the following statement (which from different perspectives may or may not be considered valid by various parties):

Static Type systems and Dynamic Type systems are the two sides of a single coin.

In the past I have raised a number of questions in this forum regarding types and programming languages that have in the main only been answered by those who have a strongly held viewpoint. I have been spending much time over the last few years considering the viewpoints thus exhibited.

The viewpoints expressed have been one of the following:

Static Type are the best - various reasoning
Dynamic Types are the best - various reasoning
Soft Typing system - amalgamation of the best of both worlds - various reasoning.

What has been unsatisfactory about the answers and the discussions that have ensued is that the subject of real world systems and the real world situations they are deployed in have not been closely examined. By this I mean that hardware related errors, system software related errors and user caused errors (including deliberate attacks) have not been brought into the discussion in relation to how the various kinds of type system can help in these conditions.

Putting aside anyone's particular bent in belief as to which is the best kind of type system for programming languages, my question is:

In what areas do each of the above type systems fail to provide the programmer with the tools (language constructs, abstraction facilities, etc.) to actually deal with real world troubles, problems and conditions?

PLT should be about improving what we can actually do with the computing machinery that we use.

With the wide range of people in this forum, what areas of research are being looked or not looked in this regard?

An example problem is an application that works correctly on a single processor system but exhibits somewhat random behaviour on a dual (or more) processor system due to the seemingly random interactions/responses of a third party library or component.

Please, not interested in ideological wars over this.

It is sometimes claimed in the FP community that explicit representation controls (unboxing) are unnecessary, because a good optimizer can re-arrange the data structures into unboxed forms where appropriate (I disregard hardware interaction for this discussion). Litmus questions here:

1. While there are definite successes here, are they real or are they a case of unrealistic benchmarks? Knowing something of the PL.8 research compiler history on this issue, I am hard pressed to believe that program-wide data restructuring will ever compete comprehensively with human prescription. Both would seem to have their place.

2. Assuming that exclusively compiler-based data structure optimization is realistic, is it feasible in the absence of whole-program analysis (issue: dynamic libraries are not optional in the real world)?

3. Again assuming that exclusively compiler-based data structure rearrangement is realistic, is there a reasonable expectation that we can characterize and specify this type of optimization well enough that independently crafted, conforming compilers will exhibit more or less consistent behavior (may exceed, but will do at least transforms X, Y, and Z)?

4. If the comparative metric is performance compared to C rather than performance compared to non-repr-optimized Haskell/ML/O'Caml, is there any comprehensively credible evidence that compiler-driven repr rearrangement is both good enough and predicable enough (in the eyes of the developer) to render prescriptive specification unnecessary? Is there robust evidence that it isn't sufficient?

   I'll settle for promising partial evidence, provided the approach admits an eventual generalization. I'm aware of TIL, and of Xavier Leroy's paper assessing effectiveness of type-driven unboxing, and of the earlier work on PL.8. The conclusions to date suggest to me that leaving this optimization exclusively to the compiler is not likely to be good enough.

Thoughts and references?

Programmable Concurrency in a Pure and Lazy Language, Peng Li's 2008 PhD dissertation, is a bit more implementation focused than is common on LtU. The paper does touch on a wide range of concurrency mechanisms so it might have value to any language designer considering ways to tackle the concurrency beast.

First, this dissertation presents a Haskell solution based on concurrency monads. Unlike most previous work in the field, this approach provides clean interfaces to both multithreaded programming and event-driven programming in the same application, but it also does not require native support of continuations from compilers or runtime systems. Then, this dissertation investigates for a generic solution to support lightweight concurrency in Haskell, compares several possible concurrency configurations and summarizes the lessons learned.

The paper's summary explains what I like most about it:

the project ... solves a systems problem using a language-based approach. Systems programmers, Haskell implementors and programming language designers may each find their own interests in this dissertation.

Even if concurrency isn't your thing, section 6.3 describes the author's findings on the pros and cons of both purity and laziness in a systems programming context.