Re: survey of projects using Sala actors

Thomas,
As a follow up regarding explicit representations of types for concurrency that i think many on the Scala list might have an interest in, let me suggest a connection between types and code navigation.
From developer experience to...On the one hand, i personally use to types to help me navigate code. For example, in a situation that decomposes into a code context and some code filling the hole in that context (K[C]), types help me forget about code specifics of the context (K) and focus on the specifics of the code (C) filling the hole (that demands my attention because that's the behavior i'm implementing or debugging). In other words, types help me navigate and focus attention to the place that demands it. More generally, we are all used to types guiding IDEs to support code completion and refactoring (which are also instances of this code navigation idea, in my book). 
Service discoveryi submit that this navigation idea has a wider set of use cases. In particular, systems like Hoogle and merobase suggest that types can be used to provide automated or semi-automated search mechanisms for any client to find a service provider. In other words, types seem like a great basis for service discovery. That said, the functional types say much too little to provide a good basis for selecting service providers. On the other hand, the behavioral types seem to offer a very rich language for describing properties of service providers. The types of Caires are particularly interesting in the balance between expressiveness and complexity of type checking.
To my mind these two features (developer experience: code navigation, completion and refactoring; and service discovery) far outweigh the cons of having an explicit representation of types -- especially if a type-inferencing scheme can eliminate the requirement for code annotations.
Best wishes,
--greg
On Wed, Feb 11, 2009 at 12:03 PM, Meredith Gregory <lgreg.meredith@gmail.com> wrote:

Thomas,
Many thanks for the detailed and thoughtful reply. Please note that with a suitable type-inferencing algorithm, annotations are pretty much at a minimum. Further, that is in keeping with the modern language design principles active in Haskell and Scala.
Best wishes,
--greg
On Wed, Feb 11, 2009 at 10:23 AM, Thomas Wies <thomas.wies@epfl.ch> wrote:

Hi Greg,

On Wednesday 11 February 2009 08.09:48 you wrote:
> i would be very interested in what you plan to do here. i tried many times
> to get the existing actor semantics nailed down, but couldn't.

Right now we first want to get an idea of what can be reasonably done with an
approach that keeps the annotation overhead at a minimum. We are currently
looking at the model checking problem for specific safety properties and
process calculi that model aspects of Scala actors.

> You probably already know that Luis Caires' spatial-behavioral types are a
> great starting point for doing what you're suggesting and the whole
> session-types cottage industry is also a reasonable starting point.
> (Personally, i would shy away from the Kobayashi types and TyPiCal.)
> However, without nailing down some things about the scheduling semantics
> there is no way to make the guarantees coming from the types actually apply
> to typed coded.

Thanks for the references. I was familiar with Caires' work, but haven't
looked into session types, yet.

> Moreover, you really, really can't call these things actors without
> specifying the notion of fairness at play. This is more than just a
> theoretical concern. Further, fairness and bisimulation-based arguments
> (that support the typing regimes) are closely connected.
>
> It would be totally awesome to get an SOS specification for Scala actor
> semantics.

I agree that at the end of the day we need a formal semantics for Scala actors
and an SOS would be the ideal outcome.

> If you guys want an extra pair of hands on this, give me a shout. i'd love
> to pitch in. Ever since we did Enabled-Sets for Actor mailboxes in Rosette
> i've been dreaming about types for concurrency for a mainstream language.

We are still in a pretty early state right now. Though I would be happy to
keep you updated.

Thomas

--
L.G. Meredith
Managing Partner
Biosimilarity LLC
806 55th St NE
Seattle, WA 98105

+1 206.650.3740

http://biosimilarity.blogspot.com

--
L.G. Meredith
Managing Partner
Biosimilarity LLC
806 55th St NE
Seattle, WA 98105

+1 206.650.3740

http://biosimilarity.blogspot.com