User-defined objects in Avail are similar to maps. Indeed, a user-defined object is constructed at a low level by building a map and invoking the primitive "_as object". The map that this primitive operates on must be a "map from cyclicType to all". A quick refresher on cyclicTypes is in order. They are all siblings of each other, and each one's type is itself.
But that's what a user-defined object looks like. The user-defined types are similar - they're represented as a "map from cyclicType to type". A user-defined object's type is a user-defined type with the same keys, but all the values have been replaced by those values' types.
From these constructions come the rules of Attribute Inheritance:
Given two user-defined types X and Y, X is a subtype of Y iff X has at least all the keys of Y, and for each key in Y, the value in X is a subtype of the corresponding value in Y.
For example, if a and b are cyclicTypes,
X ::= [a->integer][b->integer] as objectType; Y ::= [a->all] as objectType; Assert X <= Y; /* X is a subtype of Y */
Not only will instances of X have all the fields required by Y (field "a"), but the types of these fields are acceptable to Y (an intsance of X will have an integer in its "a" field, which satisfies Y's requirement that it be at least an "all").
Similarly, a user-defined object o has a type T iff they have the same keys and each value in o has as its type the corresponding value in T.
For example, if a, b, and c are cyclicTypes,
T ::= [a->integer][b->integer] as objectType; o : T; o := [a->123][b->456][c->789] as object; Assert o type = [a->[123..123]][b->[456..456]][c->[789..789]] as objectType;
Note that the variable o actually contains an object whose type is more specific than is required by o's declared type T. In particular, the object in o has an extra key, c, and the types of the values in fields a and b are subtypes of those required by T (that is, [123..123] is a subtype of integer, and [456..456] is also a subtype of integer).
Going from an object to its type (an objectType) can lose some information. For example,
o ::= [a->{10,11,20}] as object;
ot ::= o type;
Assert ot = [a->set [3..3] of [10..20]] as objectType;
Do you see how the fact that the set contains 11 is lost? That's ok, we expect that from a type system. The types in a type system should only provide a conservative approximation of the values used at runtime. Avail's type system just happens to be better than most at capturing this information. If you looked closely you'd see that it was the set type that was really losing information (i.e., the set type acted as an approximation of the information in the actual set).
Going from an objectType to its type (an objectMeta) won't actually lose information. In fact, there is a method "_instance" that converts an objectMeta back into its unique objectType.
ot ::= [a->set [3..3] of [10..20]] as objectType; om ::= ot type; Assert om instance = ot;
The same thing holds for an objectMeta and its type, an objectMetaMeta (the "_instance" message is polymorphic).
ot ::= [a->set [3..3] of [10..20]] as objectType; om ::= ot type; omm ::= om type; Assert omm instance = om; Assert omm instance instance = ot;
In practice I found that this is as far as I needed to go. The primary concern was that returns and requires clauses were able to capture enough information to be useful, and that the factories used for instance creation would have exact static information. The idea of static type checking is to ensure the final program being compiled satisfies type safety, even when the code used to check this is more relaxed about it. So after this level I intentionally lose information:
anObjType ::= [a->set [3..3] of [10..20]] as objectType; anObjMeta ::= anObjType type; anObjMetaMeta ::= anObjMeta type; anObjMetaMetaMeta ::= anObjMetaMeta type; Assert anObjType <= Object; Assert anObjMeta <= objectType; Assert anObjMetaMeta <= objectMeta; Assert anObjMetaMetaMeta = objectMetaMeta; /* Note exact match */
Note the last line - there are no subtypes of objectMetaMeta (except terminates), so all information about the objectMeta and its instance, the objectType, are lost at this level.