-
Notifications
You must be signed in to change notification settings - Fork 2
Language Specification (8) : Type Compatibility
Type compatibility is a relation between two types T1 and T2 that determines whether an entity e1 of type T1 may be assigned to, copied to, passed to or used together in an expression with an entity e2 of type T2.
Type compatibility thus determines the compatibility of two entities by their associated types. The compatibility relation between any two entities is congruent to the compatibility relation of their types. Any compatibility relation is always transitive, but not necessarily commutative. There are five compatibility relations.
Assignment compatibility is a relation between two types T1 and T2 that determines whether an entity e1 of type T1 may be assigned to an entity e2 of type T2. The relation is denoted by the =:
symbol, pronounced "assignment compatible to".
- T1 =: T2 ∧ e1 ∈ T1 ∧ e2 ∈ T2 ⇒ e1 =: e2
Copy compatibility is a relation between two types T1 and T2 that determines whether an entity e1 of type T1 may be copied to an entity e2 of type T2. The relation is denoted by the >:
symbol, pronounced "copy compatible to".
- T1 >: T2 ∧ e1 ∈ T1 ∧ e2 ∈ T2 ⇒ e1 >: e2
By-value passing compatibility is a relation between two types T1 and T2 that determines whether an entity e1 of type T1 may be passed to a formal by-value parameter e2 of type T2. The relation is denoted by the ≈:
symbol, pronounced "by-value passing compatible to".
- T1 ≈: T2 ∧ e1 ∈ T1 ∧ e2 ∈ T2 ⇒ e1 ≈: e2
By-reference passing compatibility is a relation between two types T1 and T2 that determines whether an entity e1 of type T1 may be passed to a formal by-reference parameter e2 of type T2. The relation is denoted by the ^:
symbol, pronounced "by-reference passing compatible to".
- T1 ^: T2 ∧ e1 ∈ T1 ∧ e2 ∈ T2 ⇒ e1 ^: e2
Expression compatibility is a relation between two types T1 and T2 that determines whether two entities e1 of type T1 and e2 of type T2 may be used together in a binary expression. The relation is commutative. It is denoted by the ○
symbol, pronounced "expression compatible with".
- T1 ○ T2 ∧ e1 ∈ T1 ∧ e2 ∈ T2 ⇒ e1 ○ e2
Assignment compatibility implies all other compatibility relations. Copy compatibility implies by-value passing compatibility. Passing compatibility implies expression compatibility.
- T1 =: T2 ⇒ T1 >: T2 ⇒ T1 ≈: T2 ⇒ T1 ○ T2
- T1 =: T2 ⇒ T1 ^: T2 ⇒ T1 ○ T2
A type regime is a set of rules that govern type compatibility.
The following type regimes are in use
Under strict name equivalence, types are equivalent if they are identical types.
- T1 = T2 ⇒ T1 =: T2 ∧ T2 =: T1
Under super-type equivalence, a type is upwards compatible with its super-type, but a super-type is not downwards compatible with its subtype.
- T1 is-subtype-of T2 ⇒ T1 =: T2 ∧ ¬ T2 =: T1
Under value type equivalence, collection types are copy compatible if their value types are compatible.
- T1, T2 ∈ Tcollection ∧ value-type T1 =: value-type T2 ⇒ T1 >: T2 ∧ T2 >: T1
Under target type equivalence, pointer types are compatible if their target types are compatible.
- T1, T2 ∈ Tpointer ∧ target-type T1 =: target-type T2 ⇒ T1 =: T2
Under structural equivalence, types are compatible if they have identical structure.
- T1 ≘ T2 => T1 =: T2 ∧ T2 =: T1
A type regime is limited if it only applies to a subset of compatibility relations.
Except for type OCTETSEQ
, all types follow strict name equivalence by default.
- ∀ T1, T2 ∈ { Tany ∖ Toctetseq | T1 = T2 } : T1 =: T2 ∧ T2 =: T1
The type regime may further be relaxed depending on the classification of the type.
An alias type is always identical to the type of which it is an alias.
- ∀ T1, T2 ∈ { Tany | T1 is-alias-of T2 } : T1 ≡ T2
A derived type is by definition incompatible with the type from which it is derived.
- ∀ T1, T2 ∈ { Tany | T1 is-derivative-of T2 } : ¬ T1 =: T2 ∧ ¬ T2 =: T1
Anonymous types with the same canonical type declaration are identical.
- ∀ T1, T2 ∈ { Tanon | T1 is-canonically-equal-to T2 } : T1 ≡ T2
Enumeration types follow strict name equivalence.
- ∀ T1, T2 ∈ { Tenum | T1 = T2 } : T1 =: T2 ∧ T2 =: T1
Enumeration types further follow super-type equivalence.
- ∀ T1, T2 ∈ { Tenum | T2 is-extension-of T1 ∨ T1 is-subtype-of T2 } : T1 =: T2 ∧ ¬ T2 =: T1
Set types follow strict name equivalence.
- ∀ T1, T2 ∈ { Tset | T1 = T2 } : T1 =: T2 ∧ T2 =: T1
Set types further follow value type equivalence.
- ∀ T1, T2 ∈ { Tset | value-type T1 = value-type T2 } : T1 >: T2 ∧ T2 >: T1
- ∀ T1, T2 ∈ { Tset | value-type T1 ⊂ value-type T2 } : T1 >: T2 ∧ ¬ T2 >: T1
Array types follow strict name equivalence.
- ∀ T1, T2 ∈ { Tarray | T1 = T2 } : T1 =: T2 ∧ T2 =: T1
Array types further follow value-type equivalence.
- ∀ T1, T2 ∈ { Tarray | value-type T1 = value-type T2 } : T1 >: T2 ∧ T2 >: T1
- ∀ T1, T2 ∈ { Tarray | value-type T1 ⊂ value-type T2 } : T1 >: T2 ∧ ¬ T2 >: T1
Record types follow strict name equivalence.
- ∀ T1, T2 ∈ { Trecord | T1 = T2 } : T1 =: T2 ∧ T2 =: T1
Extensible record types further follow limited super-type equivalence.
- ∀ T1, T2 ∈ { Textrec | T2 is-extension-of T1 } : T2 ^: T1 ∧ ¬ T1 ^: T2
Opaque pointer types follow strict name equivalence.
- ∀ T1, T2 ∈ { Topaque | T1 = T2 } : T1 =: T2 ∧ T2 =: T1
Other pointer types follow target type name equivalence.
- ∀ T1, T2 ∈ { Tpointer ∖ Topaque | target-type T1 = target-type T2 } : T1 =: T2 ∧ T2 =: T1
Extensible record pointer types follow super-type equivalence.
- ∀ T1, T2 ∈ { Trecptr | T1 is-extension-of T2 } : T1 =: T2 ∧ ¬ T2 =: T1
Given pointer types T1 and T2, T1 is a type extension of T2 if the target type of T1 is a type extension of the target type of T2.
- ∀ T1, T2 ∈ Trecptr : T1 is-extension-of T2 if T1′ is-extension-of T2′
where T1′ = target-type T1 ∧ T2′ = target-type T2
Procedure types follow structural equivalence.
- any two procedure types are compatible if their signatures match
- the type of a procedure is the anonymous procedure type that matches its signature
Numeric types follow strict name equivalence.
- ∀ T1, T2 ∈ { Tscalar | T1 = T2 } : T1 =: T2 ∧ T2 =: T1
Numeric subrange types follow super-type equivalence.
- ∀ T1, T2 ∈ { Tscalar | T1 is-subtype-of T2 } : T1 =: T2 ∧ ¬ T2 =: T1
Machine types follow strict name equivalence only.
- ∀ T1, T2 ∈ { Tmachine | T1 = T2 } : T1 =: T2 ∧ T2 =: T1
Address types follow strict name equivalence only.
- ∀ T1, T2 ∈ { Taddress | T1 = T2 } : T1 =: T2 ∧ T2 =: T1
The compatibility of a literal value cannot be determined by type because literals are not associated with any specific type. Instead, literal compatibility is defined as follows:
A literal value L is compatible with type T if L does not overflow T and if
- L is a character code literal and T is a character type, or
- L is a whole number literal and T is a machine type, cardinal type or integer type, or
- L is a real number literal and T is a real number type, or
- L is a non-empty structured literal and structurally equivalent to T
An empty structured literal L is compatible with type T if
-
L is the empty string
""
and T ∈ Tstring, or -
L is the empty collection
{}
and T ∈ Tset ∪ Tarray ∖ Tstring
Type compatibility is a relation between two types T1 and T2 that determines whether an entity e1 of type T1 may be assigned to, copied to, passed to or used together in an expression with an entity e2 of type T2.
Type compatibility thus determines the compatibility of two entities by their associated types. The compatibility relation between any two entities is congruent to the compatibility relation of their types. Any compatibility relation is always transitive, but not necessarily commutative. There are five compatibility relations.
Copyright © 2015-2018 Modula-2 Software Foundation