Cours The Modula-3 Type System, tutoriel & guide de travaux pratiques en pdf.

The Subtype Relation

Modula-3 is “strongly-typed”. Ideally, this means that the value space is partitionedinto types, variables are restricted to hold values of a single type, and operations are restricted to apply to operands of a fixed sequence of types. In actuality, things are more complicated. A variable of type CO..91 can safely be assigned to a variable of type INTEGER,but not vice versa. Operations like absolute value apply both to REALSand INTEGERS,instead of to a single type (overloading). The types of literals (for example, NIL) may be ambiguous. The type of an expression may be determined by how it is used (target-typing). Type mismatches may cause automatic conversions instead of errors (as when a fractional real is sounded upon assignment to an integer).
We adopted several principles in order to keep Modula-3’s type system as uniform as possible. First, there are no ambiguous types or target-typing: the type of every expression is determined only by its subexpressions, not by its use. Second, there are no automatic conversions. In some cases the representa-tion of a value changes when it is assigned (for exam-ple, when assigning to a field of a packed record) but the abstract value itself is transferred without change.
Third, the rules for type compatibility are defined in terms of a single subtype relation, written “<:“. A naive plan for doing this goes as follows:
l define T <: U by rules relating to the syntax of 203 T and U;
l define, for each type, the set of values of that type.
in such a way that these diefinitions satisfy
l Value set rule: T <: U if and only if every value of type T is a value of type U;
l Natural assignment rule: A T is assignable to a
UifandonlyifT <: U.
This plan would lead to a highly uniform type system, but unfortunately it is too simple. For example, the natural assignment rule would forbid the assign-ment of an INTEGER to a CO. .Sl ; but the conven-tional policy is to allow such an assignment, compil-ing a runtime check. We have no doubts that the conventional policy is the best one, so the natural assignment rule will not do. Any assignment satis-fying the natural assignment rule is allowed, but in addition there are more liberal rules for ordinal types (integers, enumerations, and subranges), references, and arrays. These will be described below.
We were also forced to drop half of the value set rule: if T <: U, then every value of type T is also a value of type U, but the converse does not hold. This still provides a criterion for checking that a syntac-tic subtype rule is consistent with the semantics of the types involved, but it allows us to leave out some subtype relations that are logically possible but pragmatically unattractive, because they would force the implementation to do too much work.
We will now describe the subtype rules for each class of types.

Ordinal types

Subrange types are subtypes of their “base” types, since each member of a subrange is also a member of the corresponding base type:
Cn . . ml < : INTEGER if n and m are integers
[a..b] <: E ifaandbarefromthe enumeration type E
Moreover, two subrange types are in subtype relation when their respective sets of values are in inclusion relation:
[a. .bl <: cc . . d] if [a.. . b] is a (possibly empty) subset of Cc. .dl
Note that partially overlapping subranges are com-pletely unrelated.
3.2 Set t,ypes.
For the subtype rule for sets we simply use the value set rule:
SET OF T <: SET OF T’ if T <: T’
This rule is very natural, although open to the objection that it requires the implementation to convert between representations for some assignment opera-tions.

Reference types

A reference type is either traced or untraced. A mem-ber of a traced reference type is traced by the garbage collector; that is, the implementation stores its refer-ent in a system-managed storage pool, determines at runtime when all traced references to it are gone, and then reclaims its storage. A member of an untraced reference type is not traced by the garbage collector.
The type REF T is the type of all traced references to variables of type T; the type UNTRACED REF T is the type of all untraced references to variables of type T. The type REFANY is the type of all traced references; the type ADDRESS is the type of all untraced refer-ences; and the type NULL is the type containing only NIL.
The subtype rules for reference types are again de-termined by the value set rule:
NULL <: REF T <: REFANY
NULL <: UNTRACED REF T <: ADDRESS
Notice that the value NIL is a member of all refer-ence types. This does not mean that the type of NIL is ambiguous: its type is NULL, which is assignable to all reference types by the natural assignment rule.
The TYPECASE statement can be used to determine the referent type of a variable of type REFANY, but there is no corresponding operation for variables of type ADDRESS. This difference reflects the fact that traced references must be tagged for the benefit of the garbage collector.
Untraced references are provided for several rea-sons. Low-level code may require pointers to device control blocks that do not reside in the system stor-age pool; linking with code that was compiled from another language may require pointers that are not valid traced references; and untraced references can provide significant performance advantages. Most op-erations on untraced references are type-safe. How-ever, reclaiming the storage for an untraced reference is a potential unchecked runtime error, and so is not allowed in safe modules.
Object types are also reference types, but their sub-typing rules will be described in a later section.