Avail Method Lookup Rules

Avail is a multiply polymorphic language with a parametric type system that has user defined types, link-time type restrictions, and call site specific type propagation.

In addition, metacovariance is a feature of all types in Avail.

Avail is multiply polymorphic. That means that when a message is sent, all arguments participate in determining which method to invoke. As an example, we define standard fruit arithmetic. Assume we have two types, apples and oranges, each of which is a subtype of fruit.

Method "_+_" is [a : apples, b : apples |
        .......
] : apples;

Method "_+_" is [a : apples, b : oranges |
        .......
] : fruit;

Method "_+_" is [a : oranges, b : apples |
        .......
] : fruit;

Method "_+_" is [a : oranges, b : oranges |
        .......
] : oranges;

These four combinations are sufficient for adding any combination of apples and oranges. Note that the first argument is not special, as both arguments participate symmetrically in method lookup. If both arguments at a call site are apples, the first method will be used. If the first argument is oranges and the second argument is apples, the third method will be invoked.

If oranges have no interesting properties beyond those of ordinary fruit, we can just model apples and fruit (where apples is a specialization of fruit)...

Method "_+_" is [a : apples, b : apples |
        .......
] : apples;

Method "_+_" is [a : apples, b : fruit |
        .......
] : fruit;

Method "_+_" is [a : fruit, b : apples |
        .......
] : fruit;

Method "_+_" is [a : fruit, b : fruit |
        .......
] : fruit;

This scheme lets us add apples to apples to get apples, and lets us add any other combination of fruit and apples to get fruit. If the second and third implementations are the same as the fourth one, we may as well write...

Method "_+_" is [a : apples, b : apples |
        .......
] : apples;

Method "_+_" is [a : fruit, b : fruit |
        .......
] : fruit;

Now adding apples and apples will be handled by the first method, and fruit plus fruit will be handled by the second. Adding apples and fruit will use the second method, as the first method's second argument requires apples and we passed it mere fruit. The second method is applicable because we're allowed to pass more specific things than a method expects. The lookup algorithm always picks the most specific matching method. If more than one method is appropriate and neither is more specific than the other, then an ambiguity error will be reported (at runtime for the moment).

Got it? Good. Orange you glad you read this example?

Avail has a parametric type system. A parametric type is a composition of several types into a new type by a mechanism other than simple inheritance. In Avail one can have a bag of integers, a bag of strings, an array of strings, or a bag of arrays of integers. These are all valid types (that may also happen to be related by inheritance). One could also have a map from strings to bags, or a map from integers to integers, showing that we can have multiple dimensions of parameterization.

So if we have all these kinds of collections, how do we define general operations like "_size" and "_do_"?

Well, these families of related types are best built with attribute inheritance, which is a whole 'nother story.

Avail supports user defined types.

General user defined types fall under the category of attribute inheritance.

Besides the general user defined types, there are parametric system metatypes that can be instantiated by the user any number of ways to produce interesting types. These type families include closure (block) types (like [all,integer]->set) and container (variable) types (like &:integer), among others.

Avail has provisions for link-time type restrictions at a call site.

Let's say we're defining an operation _do_ for iterating over the elements of a collection. We can write:

Method "_do_" is [c : collection, b : [all]->void |
        .......
] : void;

Let's use it to find out the total number of chocolate chips in a jar full of cookies...

total : integer;
total := 0;
jarOfCookies do [aCookie : cookie |
        total := total + aCookie chipCount;
] : void;

Method "_don't_" is [c : collection, b : [all]->void |
        b(5);
] : void;

This, by itself, is a valid method. But if we invoke _don't_ instead of _do_ we get...

total : integer;
total := 0;
jarOfCookies don't [aCookie : cookie |
        total := total + aCookie chipCount;
] : void;

This should be prevented, as the block would be invoked with the integer 5, which will be sent the message _chipCount. This situation can not be detected at compile time as both pieces of code are perfectly fine on their own. It's only allowing that block to be bound to the variable b that's the problem. Fortunately the rule of contravariance for arguments of a block prevents this.

So how do we fix the problem? If we weaken the declaration "aCookie : cookie" to "aCookie : all" we can no longer safely send it the _chipCount message (aCookie could end up being the integer 5 again). If we strengthen the condition in _do_ (by weakening the block's argument type to cookie), we'll have an iterator that'll only work for cookies, which is not much of a solution. Obviously traditional types are inadequate to solve this problem.

We use a powerful tool to solve this problem - a runtime downcast. The *_?:=_ operator takes a container and a value and attempts to do an assignment. If the actual runtime types of the variable and the value are consistent, then the assignment takes place. Otherwise a runtime error results (and the assignment does not take place). A similar method to this is the _apply_ operator which applies a block to a tuple of arguments (one invocation using all the arguments). The _apply_ method waits until runtime to check the actual arguments' types against the actual block's type. Even checking for the right number of arguments is left until runtime. The third downcast mechanism is to use cast_into_otherwise_. This operation checks if the passed block will accept the passed object, and if so, invokes the block. The argument inside the block, of course, can have a more specific static type than the expression being passed in, which produces the desired downcasting. The (optional) otherwise clause is invoked if the block would reject the argument. We can use _apply_ to bypass static type checking (postponing it to runtime)...

Method "_do_" is [c : collection, b : [terminates]->void |
        .......
        b apply <c[i]>;   /* or something similar */
        .......
] : void;

This, unfortunately, has postponed the type checking all the way to runtime (which is probably not a good idea). We can put up a safety net to catch errors at link-time (when a call-site is type checked). This is done by using Mehod_is_requires_ ...

Method "_do_" is [c : collection, b : [terminates]->void |
        .......
        b apply <c[i]>;   /* or something similar */
        .......
] : void
requires [colTp : collectionType, blkTp : closureType |
        /* ensure the collection element type matches the block's argument type */
        colTp elementType <= blkTp [1];
] : boolean;

The requires clause takes the same number of arguments as the body, but its arguments are meta-shifted up one level - that is, if an integer is passed to the body, the type integer itself is passed to the requires clause. These types are the types extracted from a call site during type checking - which is when the requires block is invoked. If the requires block answers false then the call site is considered to have a compile-time type error. If it answers true, the call site is ok (pending other considerations). Actually, all requires blocks that are known statically to apply are tested at link time (even for methods known to be occluded) so that no requires constraint can be bypassed by a more specific implementation. We have made the code safe again, unless we made a mistake in the requires clause, but hopefully that will be much less frequent than if we had disabled typechecking entirely.

To recapitulate:

1. We encountered a problem the type system could not solve directly.
2. We postponed one typecheck normally done at compile-time until run-time.
3. We introduced a requires clause which does a type check at linkage-time, making the system statically type-safe again.

Avail has call site specific type propagation.

Let's say we want a _pick method for collections that simply returns one arbitrary element (or fails if there are none). We may try writing it as:

Method "_pick" is [c : collection |
        .......
        element : all;
        element := ......;    /* pick one somehow, probably representation-specific */
        element;
] : all;

While this would work, we'd end up with something statically typed as "all" at a call site (the call to _pick). We could subclass it so that a more specific element type could be propagated back at compile time:

Method "_pick" is [c : collection of moist towellette |
        .......
        element : moist towellette;
        element := ......;    /* pick one somehow, probably representation-specific */
        element;
] : moist towellette;

But that would be silly. Rather than resort to a lazy infinite set of methods like C++ does with templates, we can instead choose to strengthen the return result when we think we know better, by using Method_is_returns_ ...

Method "_pick" is [c : collection |
        .......
        element : all;
        element := ......;    /* pick one somehow, probably representation-specific */
        element;
] : all
returns [ct : collectionType |
        ct elementType;
] : type;

Ok, that last part was a bit of a jump. The returns block takes the same number of arguments as the body, but its arguments are meta-shifted up one level - that is, if an integer is passed to the body, the type integer itself is passed to the returns block. These types are the types extracted from a call site during type checking, which is when the returns block is invoked. The type returned by the returns block (at "link time", when a call site is being compiled) is the type the compiler will use for the result type of the call. This type is embedded in the code at the call site, and is verified at run time. This lets a programmer make a strengthening claim about return type that the call site can verify (right after an actual call completes) at runtime. The run time type check after the call can, in theory, have a zero or even negative cost, as an optimizing recompiler can make use of the fact that after that position in the code, the value returned definitely satisfies that type constraint. Further uses of the value might be inlined safely without any additional type guards.

At a call site we figure out the set of all method implementations that are guaranteed to apply (based on the static types of the arguments), and run the return blocks (where available) for each of these. We then take the intersection of these types (all of which are required to hold simultaneously), producing (still at link-time) the final type-constraint for the call site. Code is generated at the call site to do a dynamic type verification after the call returns. The compiler is then free to assume that either the verification fails and a runtime type exception occurs, or the verification passes and we get a result consistent with our expectations. Regardless, if the instructions after the call and verification are reached, we know the result's type complies with expectations. Thus, the compiler is safe to assume the call plus type verification always yield something satisfying the type specified by the returns clause(s). If, for instance, this result is fed into another message send, this next call site will use our strengthened result type for the static type of that argument. Thus,

c : collection of moist towelettes;

c pick moisten;

Worried about metacovariance? Let me ease your mind.

Let's say we're building an abstract collection type that is parametric with respect to element type (i.e., the members of these collection instances satisfy a particular type constraint). Say this is handled by a metatype called collectionType. All subtypes of collection are expected to support the _elementType message (sent to the subtype itself). Ok, what happens if we have an actual collection (instance) and we want to see what _elementType its type reports. Let's further assume that the implementation of "_type" looks like this:

Method "_type" is [obj : all |
        Primitive ...;
] : type;

If we ask "aCollection type elementType", we will get a type error, as the expression "aCollection type" has the static type "type", and an arbitrary type doesn't understand "_elementType"; only collection subtypes do. Instead, let's define the "_type" method as:

Method "_type" is [obj : all |
        Primitive ...;
] : type
returns [objType : type |
        objType type;
] : meta;

This has the effect of saying that invocations of the "_type" method answers an instance of the object's type's type. In the case of "aCollection type", the static type of this expression will be "collection type" (which is a meta), instances of which understand "_elementType". This should be a convincing argument that metacovariance is supported in principal.

In practice, it also requires that for every pair of types A and B for which A <= B, it is the case that A type <= B type. That is, the meta-hierarchy mimics the type-hierarchy via a kind of homeomorphism.

You probably missed it, but there's a subtle problem with that definition of "_type". The returns clause contains an invocation of "_type", when we're still in the process of defining it! We can use a forward declaration as follows:

Forward "_type" for [all]->type;

Method "_type" is [obj : all |
        Primitive ...;
] : type
returns [objType : type |
        objType type;
] : meta;

This says that until the definition occurs (which must be in the same module), allow compilation of calls to "_type" with "all" as the argument type, and using "type" as the result type. The method should not actually be invoked until it is defined, or an error will occur. The actual method definition must have the same basic return type as in the forward declaration (as well as argument types, of course), but it can provide a returns clause to strengthen it (and a requires clause to strengthen preconditions, which similarly only applies after the definition has occurred).