Type checking in Theta occurs at compile time and is based on analysis of type designators to determine whether they designate the same type. Two type designators are equal if the designate the same type and otherwise they are unequal.

Type equality is defined as follows:

- Each simple type is equal only to itself.
- Two types obtained by instantiation are equal if they are instantiations of the same (user-defined or built-in) parameterized type and their parameters are pairwise equal.
- Two routine types are equal if: both are proc or both are iter; both have the same number of arguments, and types of matching arguments are equal; both have the same number of results (yielded results for iterators), and the types of matching results are equal; both have the same exceptions, and matching exceptions have the same number and types of results.
- Two tagged types are equal if each has the same
tagged_type, the same field names in the same order, and the
type of matching field names are equal. E.g., these two types
are not equal:
record[a: int, b: int] record[b: int, a: int]

theta-questions@lcs.mit.edu