Lambda the Ultimate

I like the idea of sliders. I was just talking about another one the other day. </gratuitous self-promotion>

I do... slide about 50%. :-) The other 50% would require Epigram to be "MetaEpigram" or somesuch. That is, I see two dimensions along which I wish to slide fluidly:

1. Type vs. value
2. "Compile time" vs. "runtime"

I confess to being somewhat surprised that we still don't have a native-code version of MetaOCaml, though, and that we're still waiting for G'Caml. Imagine how nice a MetaG'Caml would be.

Anyway, I think the next killer language will combine some nice dependent typing regime (perhaps decidable, perhaps not) and multistage programming. If this language were to leverage its expressive power so as to provide the concurrency guarantees of a TyPiCal, the distributed programming and dynamic local rebinding guarantees of an Acute, and the object-capability security guarantees of an E, that would be an industry-altering event.

I find it more likely that stupidity will continue to reign supreme in the industry regardless of progress made in programming language design.

Allow me to enter as evidence that the average programmer has no (meaningful) understanding of "dependent typing" (whether decidable or not), "dynamic local rebinding", or "object-capability security".

is a compiler that (as part of code analysis/optimization) can identify conditional statements in methods/functions that give rise to dependent types. For example (in Java-lisp-esque pseudocode):

 class Stack {
    private ConsNode theList_;
    public int size () { 
      if (theList_ == null)
         return 0;
      else
         return theList_.size();
    }
    public boolean empty () { return theList_ == null;}
    public void push (Object o) 
    { 
        ConsNode c = new ConsNode (o, theList);
        theList_ = c;
    }
    public Object pop (void)
    {
        if (theList_ == null) return null;

        ConsNode c = theList_;
        theList_ = c.cdr();
        return c.car();
    }
}    

Three of the four methods above have behavior which depends on whether theList_ is null or not. A sufficiently smart compiler might be able to automagically generate a predicate type, depending on whether or not the stack is empty, without the programmer knowing just what is going on. I'm not sure if this approach would lead to any advantage, but it's one way to do predicate types. It could even be made to work on pre-existing code.

Any research on extracting predicate types out of more generic types?

While cynicism is fun, it isn't a very effective way of bringing about change.

Nice does this.

You pointed to a page which described Nice's feature of non-null references. While that feature is (ahem) nice, that wasn't what I meant.

What I meant was the ability to identify an object predicate which is often used in the various methods of an object, and refactor such into a dependent type. The object predicate does not necessarily have to be null-ness of one of the data members.

I'm not entirely sure that this would be useful. One could introduce predicate dispatch (or pattern matching) into Java with additional syntax, similar to how these things are handled in Cecil or Haskell; but that's additional syntax which must be learned. To some, the differing syntax is good (pattern matching has different semantics than a generalized if/else); to others it may force the programmer to make a distinction that perhaps the compiler should be making. (A similar argument, though not as important, as the issue of manifest vs latent typing). But it would be nice if the compiler could perform this refactoring--if for no other reason than it might increase the chance of detecting programming errors at compile-time.

... I had no idea C2's "SSC" page was so awful. You'd think that CMU CL's/SBCL's "python" compiler didn't exist, that O'Caml didn't exist, that Concurrent Clean didn't exist... I see they threw a bone to Stalin, but then disclaimed that it was "intended" for large-scale production work. Even if Siskind were to agree with that, where does that leave Bigloo or Chicken?

*sigh* Typical C apologists. And they call LISPers arrogant.

...you are encouraged to go correct the record! Or at least add your two cents. Be sure to visit the companion page As fast as C as well; it does address O'Caml. And it's equally likely to piss you off. :)

While c2 may have it's share of C "apologists" (including myself, of a sort--I don't think that Dennis Ritchie has anything to apologize for. If anyone needs to apologize, it is programmers/managers who deploy/require C in places where it's manifestly not appropriate), it is not known as a haven for C/C++ lovers. FTMP it is (or was) dominated by OO advocates--especially those who prefer dynamically-typed languages (lots of Python and Smalltalk), with a noticeable camp of Lispers. C/C++/Java are as frequently trashed on c2 as they are here. However, FP and such are woefully under-represented; I'd personally love it if folks with a stronger functional background were to show up and stir the pot a bit more.

The important thing to note about C2 is that it is a forum frequented (mostly) by industrial programmers. It isn't the vanguard of XP or design patterns like it was in the past (nor is it as scholarly as LtU), but it still is a good place to talk about programming and such, especially from the industrial perspective. As such, there may be a good deal of misinformation (or out-of-date information) about what is available on the cutting edge. Unlike many such forums, though; most of the folks on c2 are pretty intelligent--it's not place where the most enlightened topic is enterprise java beans.

Jeff Cutsinger: I find it more likely that stupidity will continue to reign supreme in the industry regardless of progress made in programming language design.

Allow me to enter as evidence that the average programmer has no (meaningful) understanding of "dependent typing" (whether decidable or not), "dynamic local rebinding", or "object-capability security".

This is absolutely the case, and precisely the motivation for addressing the issues at the level of the type system, keeping very much in mind the observation attributed to Tom Melham, "Formal methods will never have a significant impact until they can be used by people that don't understand them," and Benjamin Pierce's observation that "Modern software engineering recognizes a broad range of formal methods for helping ensure that a system behaves correctly with respect to some specification, implicit or explicit, of its desired behavior... At the other end are techniques of much more modest power—modest enough that automatic checkers can be built into compilers, linkers, or program analyzers and thus be applied even by programmers unfamiliar with the underlying theories." The thing that E, in particular, gets deeply right is their goal of making the secure way the obvious way. TyPiCal can be described as "if you write deadlocking or racing code, your compiler will tell you," and "dynamic local rebinding" is "hot-swapping code and/or data." "Object-capability security" is "patterns of cooperation without vulnerability." The trick would be to do all of this with a syntax that would be comfortable to the C/C++/Java/C# communities.

I'm quite confident that if you made a C/C++/Java/C#-syntaxed language that made concurrency, persistence, live-upgrade, and safe cooperation among mutually-distrustful parties dead-simple, the world would, in fact, beat a path to your door.

You couldn't be closer to the truth. One of the greatest problems is that most programmers don't have a clue on formal computer science. You tell them 'lambda calculus', and they stare you as if you talk a foreign language.

(disclaimer: I am from Greece, so the above applies in my country, as well as France that my company has business with).

Let me give an example.

A colleague of mine was trying to code a routine that converts money to text; you know the stuff: '$20,156' as 'twenty thousand one hudrend fifty six dollars'. After lots of trying through if-then-else spaghetti, he finally came up with the following idea: he was about to make an object-oriented library, in which each object implemented an interface (it was in Java, by the way) that did the conversion. He made separate classes for each different type of output. When he asked about my opinion, I freaked out! it was more than 5 pages long! I said I can do the same thing with simple functions in 10 lines of code! And I did, in C++, using a 'functional' style: the conversion function simply iterated over the string, converting each digit using lookup tables according to digit position; it was a sort of 'pattern matching', without the elegance, of course, of funcional languages.

You have to see their faces when I turn their code from 100s of lines of Java code into 10s of lines of C++ functional style code! and that would be much less if I could use a functional language, but they wouldn't understand it at all.

Anyway, to cut the long story sort, stupidity in the business sector will never go away, unless the academia takes the leading role and educate the world.

Personally, although I am not related to academia (I code for a living), I have found the (programmer's) paradise in LtU. I prefer to let work behind in order to read an interesting article about programming languages: usually, the time I spend in reading LtU is earned tenfold by using some technique I find in one of the links from this site.

By the way, (and I don't know if I should say this, but I will anyway), object-oriented languages have miserabl y failed. In order to do anything clever in Java, you have to code, code, refactor, code and code again! Way too much code, even for the simplest of ideas!

Sorry for the bla bla, I just had to get it out. I hate to see the current situation with inferior programming languages winning the battle.

I disagree that OO languages in general suck. This is true if you consider as OO languages just the mainstreamish Java and C#, but I guess you're not considering the less used languages such as Smalltalk (or ruby or python or whatever) where functional idioms are tightly merged with the OO paradigm.

If a new language came along that were hugely superior, its early adopters could demonstrate unheard of levels of productivity and so generate a siginificant "wow" factor.
For (an extreme) example, say a couple of programmers implemented something like open office in a couple of weeks; now that would make news and everyone would want to know how they did it.
More adopters would come, more examples with "wow" factor and the cycle repeats until you do indeed end up with an industry changing event.

Perhaps another way to put it is, the rule of "worse is better" governs the mainstream, but this rule breaks down when the new thing is vastly better - it can't be ignored then.
Existing advanced languages don't provide enough "advancement" though.

I spent the whole Saturday googling for "concurrent proof logic" (and even "sequent", when despaired).

Have to read them all...

which, while geared towards concurrency features, illustrate dependent typing on some non-trivial examples

I found the use of dependent types in MSR example the most intriguing:

Dependent types offer a simple and flexible way to express the relations that hold between
keys and their owner or other keys. A key “k” shared between principals “A” and “B” will
have type “shK A B”. Here, the type of the key depends on the specific principals “A” and
“B”. Similarly, a constant “k” is given type “pubK A” to indicate that it is a public key
belonging to “A”. We use dependent types again to express the relation between a public
key and its inverse. Continuing with the last example, the inverse of “k” will have type
“privK k”.