Lambda the Ultimate

Has anybody ever used (this particular) Shannon?

With traditional notations, it is only practical to express part of the potentially precise information in a precise way. Fixing that problem can relieve a burden of distilling precise information from various informal representations and integrating it.

Types for Atomicity: Static Checking and Inference for Java by Cormac Flanagan, Stephen N. Freund, Marina Lifshin, and Shaz Qadeer:

Atomicity is a fundamental correctness property in multithreaded programs. A method is atomic if, for every execution, there is an equivalent serial execution in which the actions of the method are not interleaved with actions of other threads. Atomic methods are amenable to sequential reasoning, which significantly facilitates subsequent analysis and verification. This article presents a type system for specifying and verifying the atomicity of methods in multithreaded Java programs using a synthesis of Lipton’s theory of reduction and type systems for race detection. The type system supports guarded, write-guarded, and unguarded fields, as well as thread-local data, parameterized classes and methods, and protected locks. We also present an algorithm for verifying atomicity via type inference. We have applied our type checker and type inference tools to a number of commonly used Java library classes and programs. These tools were able to verify the vast majority of methods in these benchmarks as atomic, indicating that atomicity is a widespread methodology for multithreaded programming. In addition, reported atomicity violations revealed some subtle errors in the synchronization disciplines of these programs.

Recently I was coding up libraries in one of my hypothetical toy languages (I hope I'm not the only one :), and I came across a potentially novel (too me) type feature that might actually make sense. So naturally, I wonder if this has been examined before.

Imagine a simple type constructor Vector[T]. I would like to have Vectors be comparable for equality, but *this* feature is only possible if the actual type parameter T is also comparable for equality.

So we might have some silly syntax like this.

mixin Eq[T] is def? ==(T,T):Bool; end

class Vector[T] mix (Eq when T <: Eq) is
...some stuff...
   --
   -- Compare two Vector[T]'s for equality
   --
   def ==(rhs:Self):Bool = 
      self.len = rhs.len and 
      (_ == _).andmap(self, rhs); -- this compares the elements

...some other stuff...
end

Hopefully one gets the idea. Furthermore, what I really want is not to *require* T <: Eq, but to simply notate and elide the methods that depend upon T <: Eq, most notably avoiding writing a gazillion different Vector[T] classes, each featuring some different interesting quality of T that happens to affect an interesting quality of the resulting Vector[T].

Has any other person smarter than I am explored type systems(other than the "uber search and replace" C++ templates) that feature this kind of "capability parametrized" parametrically polymorphic type system with method elision/disqualification before?

Much thanks,

Scott

Larry O'Brien recently interviewed three of the Gang of Four about their seminal work on patterns. Larry teased the interview's readers for awhile, but he eventually asked the pressing question that most language designers ask and debate about patterns ;) Here it is:

Larry: GoF came out relatively early in the ascent of OOP as the mainstream paradigm and, for better or worse, "patterns" seem to be associated with OO approaches. You even hear functional and dynamic advocates boasting that their languages "don't need" patterns. How do you respond to that?

Erich: Just as an aside, it is also easy to forget that we wrote design patterns before there was Java or C#.

Ralph: Some of those languages don't need some of the patterns in Design Patterns because their languages provide alternative ways of solving the problems. Our patterns are for languages between C++ and Smalltalk, which includes just about everything called "object-oriented," but they certainly are not for every programming language. I don't think anybody actually says that programmers in other languages don't need patterns; they just have a different set of patterns.

Erich: Design patterns eventually emerge for any language. Design déjà-vu is language neutral. While these experiences are not always captured as patterns, they do exist. The design principles for Erlang come to mind.

Larry: Where would a person go to learn about patterns for dynamic and functional languages? Who's making good contributions?

Ralph: If by "dynamic" you mean dynamic object-oriented languages like Smalltalk, Ruby or Python, then our patterns are applicable. Functional languages require different patterns, but I don't know who is working on them.

Note: At the end of the interview, Erich says that they tried refactoring the patterns into new categories in 2005. The draft breakdown he provides (accidentally???) takes out Memento, Chain of Responsibility, Bridge, Adapter, and Observer.

As I said above these are just notes in a draft state. Doing a refactoring without test cases is always dangerous...

UPDATE: The Gang of Four have an accompanying article for the interview that they wrote as a group. See A Look Back: Why We Wrote Design Patterns: Elements of Reusable Object-Oriented Software.