Lambda the Ultimate

Via MetaPRL

Type Theoretical Foundations for Data Structures, Classes, and Objects

We will show that records and objects can be defined in a powerful enough type theory. We will also show how to use these type constructors to define abstract data structure.

Here we extend the constructive type theory with a simpler type constructor dependent intersection, i.e., the intersection of two types, where the second type may depend on elements of the first one (not to be confused with the intersection of a family of types). This new type constructor allows us to define dependent records in a very simple way.

Dependent intersection looks worth attention for many reasons, e.g. providing a simpler alternative to very dependent functions. I especially liked how it simplifies treatment of coincident labels (multiple inheritance, anyone? :).

I know there was Cω topic before. But the discussion really had more to do with Xen (XML, DB integration) than the Polyphonic C# concurrency part. I'm an Erlang newbie myself, but I already can see that asynchronous communication is the common thread to both languages and this approach is going to be big - can be used from embedded system to biz process orchestration.

Looking at the Santa Claus sample, Cω code seems to be quite compact and the syntax extension to C# is minimal. However process/thread creation is implicit, and it seems to be a little more difficult to reason. I would imagine a solution in Erlang clearer, but maybe longer.

Any thoughts/pointers on the pros and cons of different concurrency approaches? We really should have a "great concurrency shootout".