Chapter 27 of [ Fortress 1.0 beta] contains definitions of traits that take a type parameter T and are intended to constrain or describe T in some way. In fact, these traits are arranged into a hierarchy that can describe a large number of interesting behavioral properties. Typical examples (shown here in simplified form) are:

The intent was that a specific implementation trait such as String could be declared as

to express the fact that the concatenation operator on strings || is an associative binary operator (and furthermore necessarily defines equality = as an equivalence relation). When this is done, then within the definition of Associative, T in fact refers to the type that extends that instantiation of Associative. The idea was that T could then serve as a "self type".

This works fine when used as recommended. The problem with this idiom is that it fails to enforce the requirement that the first static argument to Associative must be a type that actually extends Associative with that same type as the first static argument. To be specific, there was nothing to prevent a programmer from writing

Within the definition of Associative, T refers to the String, not Foo, so T does not serve as a proper self type for this purpose.

There is actually a second problem lurking here: while we would like for T to serve as a "self type", the actual Fortress type of the self keyword within the instantiation Associative[\ String, || \] is not T but Associative[\ String, || \]. For T to serve as a true self type, we need the type of self to be T.

To solve these problems we have made three changes to the Fortress language. We expect these changes to be compatible extensions for nearly all purposes.

(A) The type of the self keyword within traits has changed

Fortress 1.0 beta says that the type of self is the type of the trait or object being declared by the innermost enclosing trait or object declaration or object expression.

Now, if the innermost enclosing such construct is a trait declaration (for a trait called, say, T), and that trait declaration has a comprises clause, and U1, U2, ..., Un are the traits mentioned in the comprises clause, then the type of self is instead (T & (U1 | U2 | ... | Un)), where & indicates type intersection and | indicates type union.

The effect of this change is to make the type of self a little bit sharper than it was before. In the special case that T comprises exactly one other type U, then the type of self is now (T & U), which simplifies to just U.

(B) The syntax of comprises clauses is generalized

Fortress 1.0 beta says that a trait reference listed in a comprises clause must be either a declared trait identifier or an abbreviated type for an aggregate expression.

Now, a trait reference listed in a comprises clause may also be either a full instantiation of a statically parameterized trait or a naked type variable that is one of the static parameters of the trait in which the comprises clause appears. Moreover, as a convenience, if the name of any specific static type parameter (call it U) of a trait appears as a naked type variable within the comprises clause of that trait, then the instance of the trait named by using all its static parameter names as corresponding static arguments to the trait is implicitly regarded as one of the bounds on that static parameter U (in addition to any other bounds it might have).

Thus, for example, given the code

an implicit additional bound is assumed for T, as if the code had been written

The comprises clause then enforces the relationship we originally desired: for any specific type Bar, every object that is of type Foo[\Bar\] will necessarily also be of type Bar. Moreover, it is not correct even to mention the type Foo[\Bar\] unless Bar in fact extends Foo[\Bar\] (either directly or indirectly). This can be used as a (correctly enforced) "self type" idiom.

(Many thanks to Sun Labs interns Justin Hilburn and Scott Kilpatrick for their key insight that using the comprises clause in this way solves the "self type" problem very nicely without introducing any new language concepts or constructs.)

(C) The set of traits allowed in a comprises clause is broadened

Fortress 1.0 beta says that a trait T with a comprises clause may be directly extended only by traits or objects explicitly mentioned in that comprises clause.

Now, the intent of a comprises clause for trait T is that if any object has type T, then it necessarily also has at least one of the types mentioned in the comprises clause for T. In order to describe this relationship more precisely, we introduce the notion of a trait (or object) being eligible to extend another trait.

Definition: a trait (or object) T is eligible to extend trait U if either:

(1) the declaration of U has no comprises clause, or

(2) T is a subtype of (and perhaps the same as) some trait mentioned in the comprises clause of U, or

(3) T has a comprises clause, and every trait (or object) mentioned in the comprises clause of T is eligible to extend U.

With this understanding, we now restate the constraint imposed by a comprises clause:

If trait (or object) T lists trait U in its extends clause, it is a static error if T is not eligible to extend U.

We also clarify the definition of type exclusion as follows:

If trait (or object) T excludes a trait (or object) U, it is a static error if either T is a subtype of U, or U is a subtype of T, or a third trait (or object) is a subtype of T and also a subtype of U.

An Example

Let's see how all this works in practice.

Note that the trait header for BinaryOperator now has a simple comprises T in place of a relatively verbose extends bound on the type parameter T, and similarly for Associative. The trait definitions are otherwise the same as before. Here is a use of the Assocative trait:

We are in the process of revising the Fortress Language Specification document. We expect to use this new "self type" idiom extensively, especially in Chapter 37.

Last week I talked a bit about the implementation of treaps that I wrote as part of our tests of the Fortress compiler. I mentioned that we were defining most operations in terms of:

split(key)

splits a treap at key, and returns a triple of a treap whose keys are less than key, the node containing key (or Empty), and a treap whose keys are greater than key.

join(r)

joins this treap to the treap r, all of whose keys are strictly larger than the keys in this treap.

Last week we looked at the definitions of these operations. This week we'll take a quick look at the operations we can derive from them. Then I'll dive into some optimizations --- both at the program level (adding special leaf nodes to the data structure) and at the compiler level (turning recursion into iteration!).

Combining Treaps

Our goal is to define map union, intersection, and difference on treaps. It's worth taking a step back here to note that all of these operations have a common structure:

• Handle the case where the left argument is empty
• Handle the case where the right argument is empty
• Handle the case where a given key is in both maps

We abstract this as a trait:

We could have defined the operations elementwise: handle a key in the left map alone, in the right map alone, or in both maps. However, the above formulation is more efficient: we can handle entire subtrees in bulk without traversing them. However, this implementation is not particularly well suited to being exposed in an external api, as it lays bare the internal structure of the tree. Here's the implementation of combine:

As we saw last week, writing in a pure OO style and obeying strong typing makes the code a bit more complicated as we need to detect and handle empty arguments (to avoid copying subtrees unnecessarily) and to detect and handle non-overlapped keys (this is what combineRootL/R are doing).

Note the parallelism in the above code: in combineNE and combineNEH there are recursive calls to combine that are performed in parallel.

Unusually, we define single-key operations in terms of these bulk aggregate operations as follows:

We could just as easily have given definitions in terms of split and join, but these are easier to read and have much the same net effect. Note in particular that the above definitions actually push the inserted node down the tree to the point of insertion, and then split the tree at the insertion point. This should be slightly more efficient than splitting from the root and joining back together again---though this code has a number of simplifications that mean that it really isn't worth finding out yet!

Optimization: a leaf node

One of my interests in writing this code was to explore adding aggregate leaves (containing more than one key/value pair) to a treap. We're not there yet, but the code in the repository contains a special Leaf1 node that contains a lone key/value pair; it works just like a Node with empty left and right subtrees. We restrict the combine operation in CombiningOp to arguments of type Leaf1, and add a trait NonEmpty that replaces the type Node in many of the method type signatures.

The chief savings of leaf nodes is in space, rather than time. It requires a bit less time to allocate them and fill them in, and reduces memory footprint quite a bit, but it increases the number of code paths in the various operations.

Optimization Opportunity

In the  work of Reid-Miller and Blelloch there are several mentions of iterative treap algorithms. The most intriguing is a tail-recursive split operation. The code they present passes in pointers to locations where the results of the split operation will be written; we construct the result from the top down, writing a reference to a child into its parent before all of its children are computed. Let's look at how we can accomplish this in Fortress.

Here's the original code for split (without the leaf node optimization):

Here's a few observations about the results of recursive calls to split:

• The middle result (the matching node) is always passed back out unchanged.
• The left result is either passed back unchanged, or it becomes the rightmost child of a fresh node that forms the left result of the caller.
• Similarly, the right result is either passed back unchanged, or it becomes the leftmost child of a fresh node that forms the right result of the caller.

So we can compute the split iteratively if we make the fields of a Node mutable, and pass in a node whose right will receive the left result, and a node whose left will receive the right result. We'll return the node whose key matches. If we write this by hand, the code will look something like this:

The above reformulation of split is tail-recursive; many of you will realize that the JVM is not properly tail recursive, and our tail calls are in any case virtual method calls. There's some opportunity for compiler analysis here: the Fortress compiler should transform this into a typecase and a while loop, a bit like the following:

Note that the control structure of the above code is rather messy, though, due to the fact that there are two exit paths and two continuing paths through the loop. We end up doing all the work in the condition! Even adding something like the C do/while construct won't really help us here. It would be far better if we could rely on the compiler to do this final transformation---and nicer still if the compiler also performed the first transformation for us as well.

Immutability and the Memory Model

From the perspective of someone using the Treap library, a treap is an immutable, persistent data structure. But the transformation we performed above required us to make the left and right field of every node mutable! We know that we are using this mutability in a very controlled way---we mutate a field at most once, and we do so before that field is ever examined by anyone else.

If you write something like the above code in the Java^TM programming language, you might be rather surprised to discover that it doesn't work on your multiprocessor machine. It's possible to obtain a reference to a Node (via a data race, admittedly), and then examine the resulting Treap and discover that portions of it appear to be missing, and appear to change over time. This is because we are initializing fields of a pointed-to object after it has been pointed to.

By contrast, the original pure code has no such problems. Stores into final fields in a constructor are special, and are considered to occur after pending stores into the objects pointed to by the fields, and before the object reference is made available to subsequent computations (this is nicely explained in Doug Lea's  Java Memory Model cookbook). Thus, while a treap might be involved in a data race, it will always appear self-consistent: either you see it properly initialized, or you don't see it at all (you see a reference to some other Treap instead).

Now, code ought to avoid data races---but it's particularly irritating for data races in your program to manifest as non-deterministic behavior by library code.

An open question here is how we can perform transformations like the ones above safely in a Fortress compiler, given the limitations of the underlying processor architecture and memory model. Is there a benefit to immutability if it forces us to use unnecessary and expensive memory synchronization instructions just to obtain the "obvious" semantics from our programs? And how can we perform aggressive transformations like the one above that don't respect the boundaries of constructors?

In addition to the table markup we blogged about two weeks ago, we have now added markup to allow graphic images to be inserted in Fortress comments:

{{filename}}

The filename should end in one of the extensions .jpg or .gif or .png or some other extension that can be recognized by the pdfLaTeX \includegraphics command.

If the markup appears on a line by itself, then the image is scaled so that its width equals that of the current paragraph. Otherwise, the image is scaled to be 1 inch wide.

Images may appear in table entries.

Admittedly, there is not too much call for photographs of mountains or other geographical features in comments. But it may be helpful to include diagrams:

Normally, the image file should be in the same directory or folder as the TeX file or Fortress source file being processed. On this Project Fortress wiki, the image file may be attached to the web page that contains the Fortress source code being rendered.

This markup is compatible with  Wiki Creole 1.0. For more information, click here.

I recently wrote a small implementation of treaps in Fortress. If you look in the Fortress repository you'll see a couple of versions of the code. source:/trunk/Library/Treap.fss is a standalone treap library for use with the interpreter. source:/trunk/ProjectFortress/compiler_tests/TreapAndTest.fss is the same library with some testing code. This latter works in the compiler as of this week, and marks the first large data structure to compile and run with the compiler.

Why Treaps are Interesting

A treap is a form of randomly-balanced binary search tree. Like any binary search tree, each node is labeled with a key k. Since we're implementing a key/value map, each node also contains the unique value v corresponding to that key. The key of a given node is strictly greater than the keys of nodes in its left subtree, and strictly less than the keys of nodes in its right subtree. We find the node containing a particular key as follows:

Note that sometimes a particular key is not contained in the tree, and we return the Empty node instead.

In addition to a key and a value, a treap node contains a weight w. A treap is heap ordered with respect to the weight: in our implementation, the weight of a node is larger than the weight of any node in either of its subtrees. Each time we insert a new key/value pair into the tree, we choose a weight for its node uniformly at random:

leaf1(key: ZZ32, val: String): TreapNode =
    Node(Empty, randomZZ32(2147483647), key, val, Empty)

There's lots more to know about treaps, and you can learn more from  the Wikipedia entry, and find links to code and publications on  Cecilia Aragon's treap page.

Of particular interest to parallel programmers, though, is the work that Guy Blelloch and Margaret Reid-Miller did on  fast parallel set operations using treaps. They provide a particularly simple and clear formulation of set operations in terms of two primitive operations on a treap:

split(key)

splits a treap at key, and returns a triple of a treap whose keys are less than key, the node containing key (or Empty), and a treap whose keys are greater than key.

join(r)

joins this treap to the treap r, all of whose keys are strictly larger than the keys in this treap.

The split operation is no more complicated than the nodeWithKey operation above:

This code is simple because treaps do not need to be dynamically balanced! Most familiar binary search tree data structures have a balance invariant that must be maintained. For example, AVL and red-black trees require that left and right subtrees have approximately the same depth (though each achieves this goal in a rather different way); the tree data structures found in the Set and Map libraries in Fortress are size-balanced. Regardless of the balance metric used, however, in general we need to perform  rotations to bring the tree into balance when we add or remove nodes.

Tree rotations are relatively easy to do when we're inserting or removing a single node at a time. Things get more complicated when we want to perform set operations on our trees. Why do we care? Parallelism! We want to structure our computations to produce individual pieces of data in parallel, then combine them together. Alternatively, we can perform parallel bulk operations on large sets and maps that already exist.

With treaps, we don't need to worry about rebalancing: we just put the node with the largest weight on top. In the split code above, that means we don't need to reorganize the tree at all: the node we're looking at always has the largest weight in its subtree, so it forms the root of whichever result it belongs in.

Joining two treaps works just the same way: we put the node with the larger key at the top. The code is a bit more complicated when we write it using straight OO style, because we need to detect and handle empty subtrees while avoiding type errors:

Fundamentally, when we're joining two Nodes, we put the one with the larger weight on top, and push the other one down the appropriate subtree. Note that we can assign Empty nodes the smallest possible weight by convention and simplify the above code somewhat---however, in doing so, we'll end up copying the right spine unnecessarily in some cases.

Why treaps are balanced

Treaps are of course only probabilistically balanced. Do they give us the asymptotic behavior we would expect in the common case? They do. The best way to understand the argument is by analogy to quicksort. Quicksort is expected O(n lg n) when we choose the pivot uniformly at random from the n inputs. Now, imagine we label each of the n data points with a weight w, and choose the data point with the largest weight as the pivot in each recursive sorting step. Note that all the remaining data has a weight chosen uniformly at random from the interval [0,w). We can think of our treap as representing the pattern of work in the quicksort; each key represents a choice of pivot value, the left subtree is the left subproblem of quicksort, and the right subtree is the right subproblem of quicksort.

Note that this analogy is imperfect: it doesn't tell us why split and join operations might be efficient, for example. That requires us to argue that the tree has expected depth O(lg n), and then look at the cost of pulling a tree apart along a path (split) or joining the right boundary of one tree with the left boundary of another (join). But once we know the expected tree heights, these arguments are actually reasonably straightforward---and any tree that results from any combination of operations turns out to look just like a tree that we might have constructed from first principles using our modified quicksort algorithm.

Caveats in the current implementation

There are a few caveats here: we're wrestling with a type checker bug that prevents us from separately compiling the Treap library and its test code. Right now the Treap library implements maps from ZZ32 keys to String values; ultimately we want the library to be generic in both the key and value types, and we are well on our way to achieving this goal. Once that happens, expect a flurry of activity on the libraries front as we move most of the existing Fortress code over into the compiled world.

Another caveat is that we can't return tuples from functions yet (though we can do immediate tuple bindings (a,b,c) = (x,y,z) ). As a result the split method has been split into three: splitL, nodeWithKey, and splitR.

More to come

In a future post, I'll discuss how combining operations work, and I'll also say a few words about the leaf node optimization you'll find in the repository code.

A gap in the definition of Fortress so far has to do with the interaction of union types and coercion:

a. The type of certain conditional (or "branching") expressions such as if and case and typecase is defined to be a union type, namely the union of the types of the block expressions in its clauses ([ Fortress 1.0 beta], pages 110-113).

b. Coercion is implicitly defined for tuple types and arrow types, but not for union types ([ Fortress 1.0 beta], pages 150-151).

Coercion is currently not implemented in the Fortress interpreter. Some language features that were originally intended to be implemented through coercion are supported in the interpreter by contorting the type hierarchy in unfortunate ways; for example, it isn't quite right for ZZ32 to be considered a subtype of ZZ64, nor for ZZ64 to be a subtype of ZZ. In the future, these types, as well as the type of integer literals, will be disjoint from each other, and coercions will handle the conventional conversions among them. This is what we plan to implement in the Fortress compiler.

Another problem arises from the interaction of union types with variable declarations that do not explicitly specify a type for the variable. In the code fragment

do
  x: ZZ32 = 5
  y = if p then x else 7 end
  f(y)
end

the type of the variable y is not ZZ32, but the union of ZZ32 and the type of the integer literal 7, which is a special literal type and not any of ZZ, ZZ32, ZZ64, etc. This in turn can have surprising consequences when calling the method f.

The Sun Labs Fortress team discussed these problems this week and decided to make three changes to the definition of Fortress:

1. The rule for the type of a "branching" expression is revised to read: The type of an if expression (or other similar construct) is determined in one of two ways: If the block expression in any one clause has a type for which the types of all other clauses are substitutable (that is, either a subtype or convertible by coercion), then that type is also the type of the if expression, and coercions are performed as necessary on the values of all the other block expressions; otherwise, the type of the if expression is the union of the types of the block expressions in its clauses.

(Note that if there is a clause with a type for which the types of all other clauses are substitutable, then that clause is necessarily unique; this follows from the rules that forbid circularity of coercions and subtypes. This is a fairly conservative rule, but we think it is adequate to handle most situations of practical interest. If necessary, it could be extended compatibly by allowing the compiler to search for a unique minimal type that is not the type of any clause's block expression but for which the types of clauses are substitutable.)

2. It is a static error if a variable declaration (either top-level or local) binds a variable without specifying a type for the variable and the type of the expression that provides the value for that variable is a union type.

(Readers familiar with the Haskell programming language may find this new rule vaguely reminiscent of that language's "monomorphism restriction".)

3. If (i) type C provides a coercion from type A, and (ii) type B is substitutable for type C, and (iii) type B excludes type A, then a coercion is implicitly provided from type (A union B) to type C.

(This coercion is implemented by using the coercion from A to C if the object is of type A, and by using the coercion from B to C if B is not a subtype of C. In situations where the union type arises from a conditional expression, it is typically not necessary to perform a run-time test to determine whether the object is of type A or type B if a simple optimization is performed; see Example 3 below.)

The intent of these specific choices is to make certain common kinds of code easy to write, while trying to limit confusion in more complicated situations. If the second rule produces a static error, there are two possible workarounds: either insert one or more explicit coercions, or provide an explicit type in the variable declaration.

Example 1: The classic factorial operator

opr (n: NN)! : NN = if n = 0 then 1 else n (n-1)! end

This is technically forbidden by the Fortress 1.0 beta specification, because the type of the if expression is the union of the type NN and the integer literal type; while a return type NN is given in the code, there is no rule allowing the union type to be coerced to NN.

Under the first new rule given above, the type of the if expression is NN because the type NN provides a coercion from (nonnegative) integer literals, and under the rule such a coercion will be implicitly applied to the integer literal 1 in the then clause.

Example 2: Local variable binding, simple case

do
  x: ZZ32 = 43
  z = (if p then 17 else x)
  z+2
end

Under the Fortress 1.0 beta specification, the local variable declaration of z is permitted, but the addition z+2 will likely fail because there is no overloading of + that is explicitly defined to accept an argument of union type, there is no numeric type of which that union type is a subtype that provides a concrete definition of +, and there is no rule allowing coercion of the union type.

Under the first new rule, the type of the if expression is ZZ32 because ZZ32 provides a coercion from the integer literal 17, and there is no further difficulty.

Example 3: Local variable binding, complicated case

do
  x: ZZ32 = 43
  y: NN32 = 2^31
  z = (if p then 17 elif q then x else y)
  z+2
end

Under the Fortress 1.0 beta specification, this example likely fails for reasons similar to those in the previous example.

Under the first new rule, the type of the if expression is still a union type because neither of ZZ32 nor NN32 provides a coercion from the other. Therefore a static error always occurs according to the second new rule. We believe that it is desirable for this example to produce a static error.

One way to make this code correct is to provide an appropriate type for the binding of z:

do
  x: ZZ32 = 43
  y: NN32 = 2^31
  z: ZZ64 = (if p then 17 elif q then x else y)
  z+2
end

Then an implicit coercion can be provided under the third new rule. In practice, the compiler will then rewrite the code from something like

do
  x: ZZ32 = 43
  y: NN32 = 2^31
  z: ZZ64 = coerce[\ZZ64\](if p then 17 elif q then x else y)
  z+2
end

to something like

do
  x: ZZ32 = 43
  y: NN32 = 2^31
  z: ZZ64 = (if p then coerce[\ZZ64\](17)
           elif q then coerce[\ZZ64\](x)
                  else coerce[\ZZ64\](y))
  z+2
end

This rewriting is similar to the rewritings associated with widening coercions ([ Fortress 1.0 beta], pages 151-153).

Earlier this year we implemented Wiki formatting within Fortress comments. Following a suggestion made to us in April 2008 by David J. Biesack, we based the formatting conventions on  Wiki Creole 1.0.

Now we have added table markup to the Fortress comment formatting conventions. The tables can be very simple:

or quite elaborate:

The markup is compatible with Wiki Creole 1.0 but provides extra facilities. Cells may be left-justified, right-justified, or centered, and cells can span multiple columns. Tables may be indented so as to match the indentation structure of bullet lists. For more information, click here.

The Fortress team is going to start posting a series of announcements and news items about Fortress. Our goal is to let people know about ongoing technical discussions and decisions, as well as the current status of the implementation. We may also post interesting examples of Fortress code. We hope to put up new posts at least weekly.