Lambda the Ultimate

More goodness appears to be in store for GHC, the Haskell compiler:

We introduce a variant of System F that uses a single mechanism to enable the type preserving translation of generalised abstract data types (GADTs), type classes with associated types and functional dependencies, as well as closed type functions. The core idea is to pass around explicit evidence for type equalities, just like System F passes types explicitly. We use this evidence to justify type casts encoding non-syntactic type equalities induced by the mentioned source language features. In particular, we don't need special typing rules for pattern matching on GADTs, we can easily combine GADTs with type classes, and we can relax restrictions on programs involving associated types or functional dependencies.

From SPJ: "I intend to change GHC to use FC as its intermediate language."

Looking at it, from the very, very limited understand I have, it seems that the whole coercions being witnesses to type constraints looks similar to how proof witnesses are used in Epigram. Maybe someone more knowledgeable can explain the similarity?

An idea occurred to me the other day, and I was wondering if anyone has seen anything like it. I'm sure I can't be the only one to have thought of this. The idea is to take the type annotations that we normally have in statically typed programs and place them in a separate file. A program in a language which allows this would look like it was dynamically typed, but static typing could be added progressively by adding declarations in a separate file. A good IDE could present a merged view of the source.

The thought behind this is that languages seem to mix two concerns in the program text: 1) the form of the program, and 2) an error detection regimen enforced by the compiler. It seems that they could be decoupled. A piece of program text could, for instance, have one set of types in one program, and another set of types in another.

Note that this has nothing to do with type inferencing. The idea is do to this for a "run of the mill" dynamically typed language.

Here's a link to a blog describing the idea.

I apologize for the lame attempts at entertainment at the beginning of the blog. They, regretfully, obscure my point a bit.

In a recent podcast interview, the father of Wiki talks about little languages, scripting, social software and organizing for collaborative development. Ward Cunningham is currently the Director of Community Development at the Eclipse Foundation.

Ward discusses an evolution from using compilers for custom languages, to OOP and Smalltalk, extreme programming and agile development. He also discusses social software, global collaboration, static and dynamic typing, Eclipse and his personal approach to software development.

Playing time for the MP3 audio interview is 20 minutes.

“Stretch” Languages, or, 28 years of programming Oliver Steel

"Recently I reviewed the programming languages I’ve used over the 28 years of my programming career. The result it shown in the chart below..."

Eiffel Studio looks like a nice IDE. This might make an interesting case study of the effects of a good IDE on the popularity of a language.

The GPL'd effort has its own site:
http://eiffelsoftware.origo.ethz.ch/

It has debian packages in progress:
http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=361001

For completeness. The press release can be found here:
http://www.eiffel.com/general/news/2006/2006_04_05_pr.html

Gilad Bracha is about to set in motion a JSR that may -- in a glacially unstoppable JCP fashion -- eventually address one of my pet peeves with Java: lack of distinction between public and published interfaces. The latter terms are due to Martin Fowler [PDF, 68K]:

One of the growing trends in software design is separating interface from implementation. The principle is about separating modules into public and private parts so that you can change the private part without coordinating with other modules. However, there is a further distinction -- the one between public and published interfaces.

... The two cases are quite different, yet there's nothing in the Java language to tell the difference -- a gap that's also present in a few other languages. Yet there's something to be said for the public-published distinction being more important than the more common public-private distinction.

Or, in the words of Erich Gamma:

A key challenge in framework development is how to preserve stability over time. The more miles a framework gets the better you understand how you should have built it in the first place. Therefore you would like to tweak and improve it. However, since your framework is heavily used you are highly constrained in what you can change. At this point it is crucial to have well defined APIs and to make it clear to the clients what is published API and what internal code is. For published APIs you should commit to stability and for internal code you have the freedom to change it.

To fully appreciate the kind of pain that this JSR is intended to ease, consider how developers deal with this problem today:

• The Eclipse model, as described by Erich Gamma:

  A good example of how I like to see reuse at work is Eclipse. It's built of components we call plug-ins. A plug-in bundles your code and there is a separate manifest where you define which other plug-ins you extend and which points of extension your plug-in offers. Plug-ins provide reusable code following explicit conventions to separate API from internal code. The Eclipse component model is simple and consistent too. It has this kernel characteristic. Eclipse has a small kernel, and everything is done the same way via extension points.

  Some other projects have adopted similar conventions. For example, France Telecom is known to maintain the distinction between lib and api packages:

  • org.objectweb.jorm.comp.cmdline.api
  • org.objectweb.jorm.comp.cmdline.lib

• Unpublished javadoc.

  J2SE implementations consist of two parts:

  1. Classes and interfaces implementing the published J2SE APIs.
  2. Internal implementation artifacts that aren't meant to be exposed to users of the J2SE libary.

  Sun generates Javadoc only for the "official" classes. Implementation artifacts are undocumented are not supposed to be relied on.

Both of these approach amount to the same thing: convention. Nothing stops you from using the non-published public interfaces. It will be interesting to see what will come out of Bracha's JSR.

i have been thinking about constraint programming in terms of monads. i have just about come to the conclusion that their models can be completely captured through monadic technology. What follows is an analysis conveyed through a typical example in linear programming. The motivation for the post is to see if anyone else has come up with this analysis or if it is already well known and (hopefully) reported in the literature; or, of course, to spot problems with the formulation.

Best wishes,

--greg

It seems that linear programming (LP) and other kinds of problems factor in an intriguing way. A typical LP problem will be of the form

Objective: maximize \Sum a_i * v_i
Constraints: \Sum \Sum c_{i,j} v_i < b_j
Decision variables: v_0, ..., v_N

(Note, i'm being somewhat free with syntax in order to get to the essence of the ideas. Apologies to Haskell folks.)

Writing this information symbolically, we have

([ (a[i],v[i]) | i <- [0..N], [ ((sumS [ (c[i,j],v[i]) | true ], null), b[j]) | j <- [0..M] ] ], 0, sumT)

where

sumT :: Expr -> Expr -> |R -> |R is a traced valuation function for reducing expressions in the decision variables to real numbers

and

sumS :: Expr -> Expr -> Expr -> Expr is also a traced valuation function for reducing expressions to additional constraints

Note well: the monadic forms inside the qualifiers of the outer comprehension are intended to *generate* additional qualifiers.

The interesting notion is that every constraint problem like this decomposes into a monad together with a *traced* evaluation function, CP = (Monad, Val). In the example above we have

Monad = [ (a[i],v[i]) | i <- [0..N], [ ((sumS [ (c[i,j],v[i]) | true ], null), b[j]) | j <- [0..M] ] ]

that generates a list of pairs of array access that we want to evaluate -- via the sumT -- to the appropriate product

and Val = SumT.

A constraint solver eats a pair consisting of the monadic description, together with the sumT function. The effect of running the solver is to drive the monadic generation using the valuation function. This is the moral content of Simplex, for example.

An important point to note is that the monadic description never has to be evaluated outside of the context of a particular interpretation of some monad. Its data that has polymorphic interpretations across many potentially applicable monads. Said otherwise, it's a program with many possible (re)uses.

The reason to use a traced valuation function (essentially keeping an accumulator) is that this enables composition of models. Clearly, the monadic part has a compositional story via the usual composition of monads. The traced valuation function allows composition of the valuation functions. Thus, if we have (M1,V1) and (M2,V2), we can define

(M1,V1)o(M2,V2) = (M1oM2,V1oV2)

where V1oV2(x,acc) := V2(x,V1(x,acc)) and M1oM2 is the appropriate monad composition.

Note well that these design choices make solving a model essentially like running some form of fold. Again, returning to the example, we actually have (M,0,sumT) where sumT may be considered of type X -> A -> A. Then an expression of the form (solve sumT 0 M) is in exact analogy with (foldl fn seed list) where

* sumT takes the role of fn -- which is why it's traced -- and
* 0 is the seed to the trace and
* M takes the role of the list.

Adopting this approach seems to unify all of the different sorts of constraint programming from LP to IP to FD to SAT to ... but also to line up with a generic query notion. Specifically, the monadic form [ E | C0, ..., CN ] is seems to be just another way of saying select{ E } where { C0, ..., CN }.

If you think of it, memory allocation/de-allocation is really just side-effect, I wonder if there is a functional language that makes it explicit. Any advice is appreciated :-)

I've been thinking about languages that choose purity:

My working theory is that choosing purity wins a language a lot of zealots as its fans. What other languages chose purity? What other concepts could be unifying paradigms for programming languages?

in 2002, Todd Proebsting delivered a talk about "disruptive programming language technologies" (video) He suggested that certain ideas, when integrated into programming languages, would make those languages slower, but much more useful, and would lead to the eventual displacement of older and faster languages. The technologies he listed were:

• Parsing (not regexes)
• Undo
• Tracking program state
• Constraint solving
• Concurrency
• Database operations
• XML manipulation

How has the landscape evolved since then? It seems to me that really large or really flexible programming languages could integrate these things in libraries. There are certainly parsing libraries in C++ and Haskell, for instance, and Haskell hackers have spent a lot of time trying to integrate XML and database operations into the language.

Other languages are designed exactly for these things that Proebsting mentions: XML manipulation is prominent in CDuce, XDuce, and Scala, and in the LL2 video Proebsting proposes Erlang as a solution to the concurrency problem.

Questions:

1. The Next Big Thing might end up being Ruby on Rails. Does it fit with Proebsting's thesis?
2. What other languages are filling the gaps suggesting by Proebsting? Will any become the next big thing?
3. What other disruptive technologies have you seen in programming languages since 2002?