Gradual Typing for Objects

Gradual Typing for Objects. Jeremy Siek and Walid Taha.

Static and dynamic type systems have well-known strengths and weaknesses. In previous work we developed a gradual type system for a functional calculus named [...]. Gradual typing provides the benefits of both static and dynamic checking in a single language by allowing the programmer to control whether a portion of the program is type checked at compile-time or run-time by adding or removing type annotations on variables. Several object-oriented scripting languages are preparing to add static checking. To support that work this paper develops [another calculus], a gradual type system for object-based languages, extending the [...] calculus of Abadi and Cardelli. Our primary contribution is to show that gradual typing and subtyping are orthogonal and can be combined in a principled fashion. We also develop a small-step semantics, provide a machine-checked proof of type safety, and improve the space efficiency of higher-order casts.

The authors' previous work on gradual typing was discussed here. This brings it to an object-oriented setting which is (as the abstract points out) very directly applicable to mainstream scripting languages, at least in principle.

[Edit: This is from the types list, where the authors also added: "We will present the paper at ECOOP 2007 and would be especially interested in any feedback on the paper before the final submission is due on April 25."]

First Class Relationships in an Object-oriented Language

First Class Relationships in an Object-oriented Language, by Gavin Bierman and Alisdair Wren, was a paper published at ECOOP 2005.

They show how to add relationships as a first-class mechanism to a Java-like language, where by relationships in something like the UML sense. Cribbing from their examples, you might have a Student class and a Course class, and an Attends relationship, which is a binary relation between Students and Courses. Then, there are mechanisms to dynamically add and remove entries from a relationship, and to query a relationship about whether particular objects are in them or not.

Now my personal random editorialisation: I think this is a really interesting idea, because these kinds of things pops up all the time in OO models, and having relations be first class means that you can move some state out of individual object instances, which is always a good thing, and the type system can guarantee something about what relationships will hold. The things that scare me about this idea are first, that you can potentially add a lot of heap pressure by keeping objects live longer, and second, that you now have much more pervasive aliasing of objects in your program. I don't know if these are real problems though, and anyway the feature is cool enough that I'd be interested in programming in a language with support for it, just to see what it's like.

Directness and liveness in the morphic user interface construction environment

Directness and liveness in the morphic user interface construction environment, John H. Maloney and Randall B. Smith, 1995.

Morphic is a user interface construction environment that strives to embody directness and liveness. Directness means a user interface designer can initiate the process of examining or changing the attributes, structure, and behavior of user interface components by pointing at their graphical representations directly. Liveness means the user interface is always active and reactive-objects respond to user actions, animations run, layout happens, and information displays update continuously. Four implementation techniques work together to support directness and liveness in Morphic: structural reification, layout reification, ubiquitous animation, and live editing.

Morphic was developed in Self and then adopted by Squeak. Reading this paper makes Squeak more interesting to click around in!

Interesting project to modularize Squeak

Ralph Johnson mentions an interesting project from Pavel Krivanek to modularize Squeak. For example, there's a KernelImage that excludes the GUI (it's 2.8 MB compared to 15 MB for the full 3.9 release). The modularized images are created automatically from the complete image, by Squeak code.

It's been awhile since we discussed Squeak, which remains as far as I can tell, an interesting project worth keeping an eye on.

Is "post OO" just over?

While studying the conference program of the upcoming OOPSLA 2006 I discovered under the category "essay" an author who has quite something critical to say about AOP:

Aspect-oriented programming is discussed as a promising new technology. Like object-oriented programming, it is beginning to pervade all areas of software engineering. With its growing popularity, practitioners and academics alike are beginning to wonder whether they should start looking into or it, or otherwise risk having missed an important development. The author of this essay finds that much of aspect-oriented programming's success seems to be based on the conception that it improves both modularity and the structure of code, while in fact, it actually works against the primary purposes of the two, namely independent development and understandability of programs. Not seeing any way of fixing this situation, he thinks the success of aspect-oriented programming to be paradoxical.

This is not just another internet rant about the latest PL hype but the author, Friedrich Steimann, had done interesting work about AOP before. In particular his latest paper about typed AOP:

AOP and the antinomy of the liar

but also his award winning former critical AOP review:

Domain models are aspect free

Revealing the X/O impedance mismatch

Ralf Lämmel and Erik Meijer. Revealing the X/O impedance mismatch.

When engaging in X/O mapping, i.e., when viewing XML data as objects or vice versa, one faces various conceptual and technical challenges -- they may be collectively referred to as the `X/O impedance mismatch'. There are these groups of challenges. (i) The XML data model and the object data model differ considerably. (ii) The native XML programming model differs from the normal OO programming model. (iii) The typical type systems for XML and objects differ considerably, too. (iv) Some of the differences between data models and between type systems are more like idiosyncrasies on the XML site that put additional burden on any X/O mapping effort. (v) In some cases, one could ask for slightly more, not necessarily XML-biased language expressiveness that would improve X/O mapping results or simplify efforts.

The present article systematically investigates the mismatch in depth. It identifies and categorizes the various challenges. Known mitigation techniques are documented and assessed; several original techniques are proposed. The article is somewhat biased in that it focuses on XML Schema as the XML type system of choice and on C# as the OO programming language of choice. In fact, XSD and C# are covered quite deeply. Hence, the present article qualifies as a language tutorial of `the other kind'.

This paper is over 100 pages, way longer than I have the time to read at the moment. Skimming, the paper looks interesting and useful. If you manage to read the whole thing, do share your observations with us in the discussion group.

Securing the .NET Programming Model

Securing the .NET Programming Model. Andrew J. Kennedy.

The security of the .NET programming model is studied from the standpoint of fully abstract compilation of C#. A number of failures of full abstraction are identified, and fixes described. The most serious problems have recently been fixed for version 2.0 of the .NET Common Language Runtime.

This is highly amusing stuff, of course. Some choice quotes:

if source-language compilation is not fully abstract, then there exist contexts (think ‘attackers’) in the target language that can observably distinguish two program fragments not distinguishable by source contexts. Such abstraction holes can sometimes be turned into security holes: if the author of a library has reasoned about the behaviour of his code by considering only source-level contexts (i.e. other components written in the same source language), then it may be possible to construct a component in the target language which provokes unexpected and damaging behaviour.

One could argue that full abstraction is just a nicety; programmers don’t really reason about observations, program contexts, and all that, do they? Well, actually, I would like to argue that they do. At least, expert programmers...

"A C# programmer can reason about the security properties of component A by considering the behaviour of another component B written in C# that “attacks” A through its public API." -
This can only be achieved if compilation is fully abstract.

To see the six problems identified by thinking about full abstraction you'll have to go read the paper...

Variance and Generalized Constraints for C# Generics

Variance and Generalized Constraints for C# Generics. Burak Emir, Andrew J. Kennedy, Claudio Russo, Dachuan Yu. July 2006

Generic types in C# behave invariantly with respect to sub-typing. We propose a system of type-safe variance for C# that supports the declaration of covariant and contravariant type parameters on generic types. To support more widespread application of variance we also generalize the existing constraint mechanism with arbitrary subtype assertions on classes and methods. This extension is useful even in the absence of variance, and subsumes equational constraints proposed for Generalized Algebraic Data Types (GADTs). We formalize the subtype relation in both declarative and syntax-directed style, and describe and prove the correctness of algorithms for constraint closure and subtyping. Finally, we formalize and prove a type safety theorem for a featherweight language with variant classes and generalized constraints.

Discussion of previous C# GADT paper on LtU.

I am unsure about use-site versus definition-site variance declerations. It would be interesting to hear what others think.

Also check out the LtU discussion on wildcards in Java.

Class decorators in Python

Guido resisted the few calling for class decorators, because there wasn't a clear use case that wasn't more readable done another way... [but] Guido has conceded, class decorators will make it into some future version of Python.

More + links: here.

JOT: On The Next Move in Programming

We seem to be in denial that our industry is maturing, we are losing our elders, some of us don’t code any more and many of our new things are really good ideas from 20 or more years ago. Some good old ideas reappear because the technology is now available to commercially exploit them; others become popular because they provide a better approach to solving a particular problem. Reinvention and improvement of good old ideas is both scholarly and sound engineering provided the prior art is cited and explained as opposed to hyped or even patented. This means we need to look for the important small improvements and not just the big bang!

Nothing remarkably new in this article, but you might want to take a look. The article was inspired by The Next Move in Programming: A Conversation with Sun's Victoria Livschitz. Victoria Livschitz's ideas were discussed here in the past.

XML feed