Immutable & Isolated Types Likely in Future C#

« “In” Parameters Proposal for C# 6.0 | Main | Mads on the Future of C# (6.0) »

December 09, 2013

Immutable & Isolated Types Likely in Future C#

Based on several pieces of evidence, immutable and isolated type designators are likely in a future version of C# and the common language runtime (CLR). These features will likely debut on .NET 5.0 in the next major iteration of Visual Studio, Visual Studio 2014.

  1. Immutable types in imperative language, US patent application filed in June 2008.
  2. Type system support for memory isolation permissions, US patent grant filed in Apr 2009.
  3. Unique and Reference Immutability for Parallelism, Microsoft Research October 2012
  4. Imperative + Functional == Smile.
  5. Joe Duffy on Uniqueness and Reference Immutability for Parallelism.
  6. Perspectives on Concurrency and Parallelism. Channel 9 Expert to Expert interview with Joe Duffy and Eric Meijer
  7. Mentions by Mad Torgersen and other C# team members about potential syntax support for immutability

The first patent application on immutability describes a new class modifier keyword “immutable” in C# that requires all fields in the class be “readonly” and themselves immutable.

public immutable class String {
     public readonly int Length;
     public readonly LinkedList<char> Chars;
     ...
}
class ImmutableList<T> where T is immutable {. . . }

The second patent includes additional information about type system support for three different isolation permission modifiers. The three permissions are immutable permission, read permission and write permission. Some pseudocode is included in the patent with tentative syntax that is likely to change.

class C {
 private T:w m_f;
 public C( ) { m_f = new T( ); }
 public isolated:r T:r Get ( ) { return m_f; }
 public isolated:w void Set(T:w obj) { m_f = obj; }
}

The key developer for this feature is Joe Duffy, who is referenced in all these links. Anders Hejlsberg is also a contributor to both patents, signifying likely inclusion into a future version of C#. The immutable types patent, in fact, lists only these two persons as inventors.

The theory behind immutability and isolation is expounded on in the Microsoft Research paper. The synopsis for the paper is:

A key challenge for concurrent programming is that side-effects (memory operations) in one thread can affect the behavior of another thread. In this paper, we present a type system to restrict the updates to memory to prevent these unintended side-effects. We provide a novel combination of immutable and unique (isolated) types that ensures safe parallelism (race freedom and deterministic execution). The type system includes support for polymorphism over type qualifiers, and can easily create cycles of immutable objects. Key to the system's flexibility is the ability to recover immutable or externally unique references after violating uniqueness without any explicit alias tracking. Our type system models a prototype extension to C# that is in active use by a Microsoft team. We describe their experiences building large systems with this extension. We prove the soundness of the type system by an embedding into a program logic.

The proposed extensions to C# uses more plausible syntax with four new keywords: writable, readable, isolated, and immutable.

immutable IntBox freeze(isolated IntBox b) {
  // implicitly convert b to readable
  // implicitly recover immutability;
  // the input context was all isolated
  return b;
}
int countElements(readable ElementList lst)

Joe Duffy elaborates more on the idea in a Channel 9 interview, a blog post, and another interview with a journalist.

While it may appear that these features are motivated by parallelism, the primary focus is not implicit parallelism according to the blog post “Imperative + Functional == :- )”. Joe summarizes the goals of the new keywords and concepts with four points, one of which includes marrying the best of functional and and imperative programming styles.

  1. Create a single language that incorporates the best of functional and imperative programming. Both offer distinct advantages, and we envisioned marrying the two.
  2. Codify and statically enforce common shared-memory state patterns, such as immutability and isolation, with minimal runtime overhead (i.e., virtually none).
  3. Provide a language model atop which can be built provably safe data, task, and actor-oriented concurrency abstractions. Both implicit and explicit. This includes, but is not limtied to, parallelism.
  4. Do all of this while still offering industry-leading code quality and performance, rivaling that of systems-level C programs. Yet still with the safety implied by the abovementioned goals.

 

Comments