CS412/413 Spring 1999 Introduction to Compilers and Translators

Iota+ Static Semantics

In this handout, we provide static semantics for the Iota+ programming language by modifying the earlier Iota static semantics.

Types

Class types and interface types will be represented in type equations as the types as type N, where N is the name of the type. The actual information about the method signatures for these classes is stored in the environment in the entry A[N], which is an environment itself mapping method and field identifiers to their corresponding type signatures and types.

Type Interpretation

An issue that was implicit in the Iota rules is how to convert type expressions to types. This issue becomes interesting with the introduction of class and interface types, because these types must be looked up in the current environment when encountered to determine whether they are valid types. In other words, an identifier N, used in a position where a type is expected, should not simply be converted to an internal representation as (type N); it must be looked up in the environment first. We can represent this conversion process as a function that takes in an AST node representing a type expression and returns an internal representation of a type. The rules for Iota are reinterpreted so that all uses of type expressions T implicitly indicate the application of this type interpretation function.

Subtype Judgements

There are two judgments for type-checking in Iota+: the standard judgement present in Iota, A |– E : T, and a new judgment about subtype relationships, A |– T1 £ T2. The first judgement says that the expression or statement E has the type T. The second judgment says that is a T1 is a subtype of T2. There are certain axioms that extend the power of these judgements. First of all, there is the fundamental subsumption rule that connects these two kinds of judgments:

A |– E : T1
A |– T1 £ T2
A |– E : T2

In addition, the subtyping relation has the properties of transitivity and reflexivity, so it is a pre-order:

A |– T1 £ T2
true

A |– T2 £ T3

A |– T £ T

A |– T1 £ T3

The types void and bottom have associated subtyping axioms: A |– T £ void and A |– bottom £ T for all T. Also, the types Null and object have pre-defined subtype relations: A |– type N £ object and A |– Null £ type N for all N. Also, the types string and array[T] are subtypes of object.

Finally, we have rules for inferring subtype relations among different object types:

A[N] = class N extends N' { ... } A[N] = interface N extends N' { ... }
A |– type N £ type N' A |– type N £ type N'

Note that more indirect relationships in the subtype hierarchy are shown using the rule for transitivity.

Type-Checking Expressions

The rules for existing Iota expressions remain the same, although they become richer because of the addition of the subsumption rule. However, various new expressions have been added to the language and rules for checking them are needed.

The type of the expression this is looked up in the environment under the special name this -- A |– this : A[this] for all A. The type of the expression null is always Null -- A |– null : Null for all A.

The type of the expression new N, where N is the name of a class, is type N, but requires a check that the class N actually exists in the environment (which guarantees that its declaration was valid):

A[N] = class N ... { ... }
A |– new N : type N

The type of a field access is looked up in the environment of the class:

A |– E : type N
A[N] |– id : T
A |– E . id : T

A method call is checked by ensuring that the types of each of the actual expressions supplied as arguments are the same as the declared types of the formal arguments. Note that this rule looks in the appropriate class environment to find the signature of the function named id.

A |– E  : type N
{id : T1 ´ T2 ´ ... ´ Tn® T} Î A[N]
"(i Î [1, n]) A |– Ei : Ti

A |– E . id ( E1,...,En )  : T

Fields and methods of the pseudo-variable this may be accessed without explicitly naming the object on which they are being invoked. Special rules are needed to support these shorthands:

A[this] = type N
A[this] = type N {id : T1 ´ T2 ´ ... ´ Tn® T} Î A[N]
A[N] |– id : T "(i Î [1, n]) A |– Ei : Ti

A |– id : T

A |– id ( E1,...,En )  : T

Finally, the cast expression has exactly the type it claims to (the program halts if not!):

A |–  E  : T'
A |– cast ( E, T )  : T

Some existing Iota expressions are changed slightly. The & and | operators accept object types as arguments as well as booleans:

A |– E1 : bool  \/   A |– E1 : object  A |– E1 : bool  \/   A |– E1 : object 
A |– E2 : bool  \/   A |– E2 : object  A |– E2 : bool  \/   A |– E2 : object 
A |– E1 & E2 : bool A |– E1 | E2 : bool

The various comparison operators are typed in the same way as their already-existing counterparts in Iota.

Type-Checking Statements

Statement forms also are extended in Iota+. The subtype relation between void and other types in the type system actually makes it easier to express rules about statements.

There is a new kind of assignment statement: an assignment to a field. We will treat assignment statements as if they were expressions for the purpose of type checking. This treatment allows multiple assignment to be checked conveniently without changing the previously existing rules for checking assignment, recalling that assignment associates to the right.

A |– E1 : type N A[this] : type N
A[N] = class N ... { id : T } A[N] = class N ... { id : T }
A |– E2 : T A |– E2 : T
A |– E1 . id = E2 ; : T A |–  id = E2 : T

The new increment and decrement can be checked exactly as if they were assignments to an addition expression:

A |– E = E + 1 ; : T A |– E = E - 1 ; : T
A |– E++ ; : T A |– E-- ; : T

The if statement and while statement are augmented to allow their test expressions to be either of type bool or of type object:

A |– E : bool  \/  A |– E : object
A |– E : bool  \/  A |– E : object A |–  S1 : T
A |– S : T A |–  S2 : T
A |– if ( E ) S  : void A |– if ( E ) S1 else S2 :  T

Because of the subsumption rule, we no longer need a special rule for the case where the two arms return different types!

A while statement always has the type void, and requires that its test expression has type bool or object. In addition, a special entry is added to the environment under the keyword break. When a break statement is encountered, this entry is checked for. If the entry is not present, the break statement has occurred outside any containing while statement and is therefore illegal. The type of a break statement is bottom because the statement does not transfer control to the containing context.

A |– E : bool  \/  A |– E : object
A + { break : void } |– S : T A[break] = void
A |– while ( E ) S  : void A |– break; : bottom

A return statement is checked as before, but its result has type bottom.

A |– E : T
{ return : void }Î A { return : T }Î A
A |– return; : bottom return E ;: bottom

Modules

As in Iota, the goal of the type checker is to determine whether an entire module M is well-typed. This judgment will be written as |– M, where M is the text of the module. To check a module, we first construct an environment in which all of the module "uses" definitions and the components of the module themselves appear. This environment construction is performed by the function module-env, which must be extended to handle the new kinds of definitions found in Iota+. In Iota, the type checker effectively made two passes over the module; one to pick up the signatures of all the functions, and a second to actually check the function bodies. In Iota+, the first pass picks up the signatures of all the functions and the names of all the classes, interfaces, functions, and variables defined in the module. The second pass then checks all the method and function bodies. In the Iota semantics, the first pass was performed by the function module-env, which must be extended to handle the new kinds of definitions found in Iota+, including interface type declarations, class definitions, and constant definitions.

In addition, new rules for checking module definitions must be added to accommodate these kinds of  definition kinds. With these additions, modules can be checked in exactly the same general way as before.We can write formal rules for how to check class and interface type definitions within modules, which enforce. A class or interface type may not define any members that have the same name as any supertype member, unless the member is a method and its signature conforms to that in the supertype in the usual contravariant/covariant manner. No class members may have the same name as any function, top-level variable, class or interface in the module, either, because otherwise there would be ambiguity about what that member meant within the body of the methods of the class. Interface members may have the same names as global identifiers because they are never introduced into scope automatically.

Note that it is not possible to check even the signatures of the class declarations that are entered into the environment on the first pass, because the compiler will not necessarily know all of the types it needs to in order to understand the field and method signatures of the class. There are two ways of dealing with this problem. One approach is to enter the class and interface type definitions into the symbol tables using uninterpreted type expressions. The other approach is to add an additional pass over the symbol table that interprets all of the type expressions used in the class member signatures and replaces the symbol table entries with fully-resolved entries.

Interface Type Declarations

Let F denotes a function declaration. An interface type declaration is legal if the methods if all of its methods are conformant with those in its supertypes, if any:

A |– conformant(Fi, A[N'])
A |– [ interface N [ extends N' ] { F1,...,Fn }]

A method is conformant either if no method of that name exists in any supertype, or if a method of that name exists, but with the same number of arguments, where the arguments in the supertype method are subtypes of the arguments in the subtype method, and the return type in the supertype method is a supertype of the return type in the subtype method.

Ø$i Fi = id(...,a'j : T'j,...) : T'r
A |– conformant(id(ai : Ti) : Tr, A[N''])
A |– conformant(id(...,ai : Ti,...) : Tr, interface N' [ extends N'' ] { F1,...,Fn })

 
$i  Fi = id(a'1 : T'1,..., a'm : T'm) : T'r
"i A |– T'i £ Ti
A |– Tr £ T'r
A |– conformant(id(a1:T1,...,am:Tm) : Tr, interface N' [ extends N'' ] { F1,...,Fn })

Class Definitions

A class is checked similarly to an interface, in that method signatures must be checked for conformance. However, a class definition requires three additional kinds of checks: the members of the class may not conflict with anything in the environment, all supertype methods must be implemented by some method body, and the method bodies must be checked as well.

A' = module-env(D1,...,Dn)
A' + {this : type N} |– [ ..., Di, ... ]
(Di = (F = E)) ® A |– conformant(F, A[N'])
A |– [ class N [ extends N' ] { D1,...,Dn }]

A method in a class is checked in much the same way as a function is. There is one difference: the environment is assumed to contain a binding from this to the type of the current class. Otherwise, the same rules can be used for type-checking methods as for type-checking functions.