Chapter 3. Type system

Every value in a Ceylon program is an instance of a type that can be expressed within the Ceylon language as a class. The language does not define any primitive or compound types that cannot, in principle, be expressed within the language itself.

A class, fully defined in §4.5 Classes, is a recipe for producing new values, called instances of the class (or simply objects), and defines the operations and attributes of the resulting values. A class instance may hold references to other objects, and has an identity distinct from these references.

Each class declaration defines a type. However, not all types are classes. It is often advantageous to write generic code that abstracts the concrete class of a value. This technique is called polymorphism. Ceylon features two different kinds of polymorphism:

Ceylon, like Java and many other object-oriented languages, features a single inheritance model for classes. A class may directly inherit at most one other class, and all classes eventually inherit, directly or indirectly, the class Anything defined in the module ceylon.language, which acts as the root of the class hierarchy.

A truly hierarchical type system is much too restrictive for more abstract programming tasks. Therefore, in addition to classes, Ceylon recognizes the following kinds of type:

Although we often use the term parameterized type or even generic type to refer to a parameterized type definition, it is important to keep in mind that a parameterized type definition is not itself a type. Rather, it is a type constructor, a function that maps types to types. Given a list of type arguments, the function yields an applied type.

In light of the fact that Ceylon makes it so easy to construct new types from existing types without the use of inheritance, by forming unions, intersections, and applied types, it's often useful to assign a name to such a type.

The Ceylon type system is much more complete than most other object oriented languages. In Ceylon, it's possible to answer questions that might at first sound almost nonsensical if you're used to languages with more traditional type systems. For example:

The answers, as we shall see, are: Element?, Integer|Float, Persistent&Printable, String(Object), {String+}(String+), [String,Float,Float], and List<Nothing>.

It's important that there is always a unique "best" answer to questions like these in Ceylon. The "best" answer is called the principal type of an expression. Every other type to which the expression is assignable is a supertype of the principal type.

Thus, every legal Ceylon expression has a unique, well-defined type, representable within the type system, without reference to how the expression is used or to what type it is assigned. This is the case even when type inference or type argument inference comes into play.

Neither this specification nor the internal implementation of the Ceylon compiler itself use any kind of "non-denotable" types. Every type mentioned here or inferred internally by the compiler has a representation within the language itself. Thus, the programmer is never exposed to confusing error messages referring to mysterious types that are not part of the syntax of the language.

3.1. Identifier naming

The Ceylon compiler enforces identifier naming conventions. Types must be named with an initial uppercase letter. Values, functions, and constructors must be named with an initial lowercase letter or underscore. The grammar for identifiers is defined by §2.3 Identifiers and keywords.

TypeName: UIdentifier
MemberName: LIdentifier

A package or module name is a sequence of identifiers.

PackageName: LIdentifier | UIdentifier

Ceylon defines three identifier namespaces:

  • classes, interfaces, type aliases, and type parameters share a single namespace,

  • functions and values, including parameters, and constructors share a single namespace, and

  • packages and modules have their own dedicated namespace.

The Ceylon parser is able to unambiguously identify which namespace an identifier belongs to.

An identifier that begins with an initial lowercase letter may be forced into the namespace of types by prefixing the identifier \I. An identifier that begins with an initial uppercase letter may be forced into the namespace of methods and attributes by prefixing the identifier \i. A keyword may be used as an identifier by prefixing the keyword with either \i or \I. This allows interoperation with other languages like Java and JavaScript which do not enforce these naming conventions.

3.2. Types

A type or type schema is a name (an initial uppercase identifier) and an optional list of type parameters, with a set of:

  • value schemas,

  • function schemas, and

  • class schemas.

The value, function, and class schemas are called the members of the type.

Speaking formally:

  • A value schema is a name (an initial lowercase identifier) with a type and mutability.

  • A function schema is a name (an initial lowercase identifier) and an optional list of type parameters, with a type (often called the return type) and a sequence of one or more parameter lists.

  • A class schema is a type schema with either one parameter list, or a list of constructor schemas.

  • A callable constructor schema is a name (an initial lowercase identifier) with exactly one parameter list.

  • A value constructor schema is a name (an initial lowercase identifier).

  • A parameter list is a list of names (initial lowercase identifiers) with types. The signature of a parameter list is formed by discarding the names, leaving the list of types.

Speaking slightly less formally, we usually refer to an attribute, method, or member class of a type, meaning a value schema, function schema, or class schema that is a member of the type.

A function or value schema may occur outside of a type schema. If it occurs directly in a compilation unit, we often call it a toplevel function or toplevel value.

A value schema, function schema, or parameter list with a missing type or types may be defined. Any such schema, or parameter list with a missing type is called partially typed.

Two signatures are considered identical if they have exactly the same types, at exactly the same positions, and missing types at exactly the same positions.

3.2.1. Member distinctness

Overloading is illegal in Ceylon. A type may not have:

  • two attributes with the same name,

  • a method and an attribute with the same name,

  • two methods with the same name, or

  • two member classes with the same name.

Note: the Ceylon compiler itself is able to represent type schemas with overloaded members and reason about overloading, and does so when compiling code that calls native Java types. However, this behavior is outside the scope of this specification.

3.2.2. Subtyping

A type may be a subtype of another type. Subtyping obeys the following rules:

  • Identity: X is a subtype of X.

  • Transitivity: if X is a subtype of Y and Y is a subtype of Z then X is a subtype of Z.

  • Noncircularity: if X is a subtype of Y and Y is a subtype of X then Y and X are the same type.

  • Single root: all types are subtypes of the class Anything defined in the module ceylon.language.

Also, every interface type is a subtype of the class Object defined in ceylon.language.

If X is a subtype of Y, then:

  • For each non-variable attribute of Y, X has an attribute with the same name, whose type is assignable to the type of the attribute of Y.

  • For each variable attribute of Y, X has a variable attribute with the same name and the same type.

  • For each method of Y, X has a method with the same name, with the same number of parameter lists, with the same signatures, and whose return type is assignable to the return type of the method of Y.

  • For each member class of Y, X has a member class of the same name, with a parameter list with the same signature, that is a subtype of the member class of Y.

Furthermore, we say that X is assignable to Y.

3.2.3. Union types

For any types X and Y, the union, or disjunction, X|Y, of the types may be formed. A union type is a supertype of both of the given types X and Y, and an instance of either type is an instance of the union type.

Note: the type expression X|Y is pronounced “x or y”.

The union type constructor | is associative, so the union of three types, X, Y, and Z, may be written X|Y|Z.

UnionType: IntersectionType ("|" IntersectionType)*

If X and Y are both subtypes of a third type Z, then X|Y inherits all members of Z.

void write(String|Integer|Float printable) { ... }

Union types satisfy the following rules, for any types X, Y, and Z:

  • Commutativity: X|Y is the same type as Y|X.

  • Associativity: X|<Y|Z> is the same type as <X|Y>|Z, where the angle brackets denote grouping.

  • Simplification: if X is a subtype of Y, then X|Y is the same type as Y.

  • Subtypes: X is a subtype of X|Y.

  • Supertypes: if both X and Y are subtypes of Z, then X|Y is also a subtype of Z.

The following results follow from these rules:

  • X|Nothing is the same type as X for any type X, and

  • X|Anything is the same type as Anything for any type X.

Finally:

  • If X<T> is covariant in the type parameter T, then X<U>|X<V> is a subtype of X<U|V> for any types U and V that satisfy the type constraints on T.

  • If X<T> is contravariant in the type parameter T, then X<U>|X<V> is a subtype of X<U&V> for any types U and V that satisfy the type constraints on T.

3.2.4. Intersection types

For any types X and Y, the intersection, or conjunction, X&Y, of the types may be formed. An intersection type is a subtype of both of the given types X and Y, and any object which is an instance of both types is an instance of the intersection type.

Note: the type expression X&Y is pronounced “x and y”.

The intersection type constructor & is associative, so the intersection of three types, X, Y, and Z, may be written X&Y&Z.

IntersectionType: PrimaryType ("&" PrimaryType)*

The intersection X&Y inherits all members of both X and Y.

void store(Persistent&Printable&Identifiable storable) { ... }

Intersection types satisfy the following rules, for any types X, Y, and Z:

  • Commutativity: X&Y is the same type as Y&X.

  • Associativity: X&<Y&Z> is the same type as <X&Y>&Z, where the angle brackets denote grouping.

  • Simplification: if X is a subtype of Y, then X&Y is the same type as X.

  • Supertypes: X is a supertype of X&Y.

  • Subtypes: if both X and Y are supertypes of Z, then X&Y is also a supertype of Z.

  • Distributivity over union: X&<Y|Z> is the same type as <X&Y>|<X&Z>.

The following results follow from these rules:

  • X&Nothing is the same type as Nothing for any type X, and

  • X&Anything is the same type as X for any type X.

Finally:

  • If X<T> is covariant in the type parameter T, then X<U>&X<V> is a supertype of X<U&V> for any types U and V that satisfy the type constraints on T.

  • If X<T> is contravariant in the type parameter T, then X<U>&X<V> is a supertype of X<U|V> for any types U and V that satisfy the type constraints on T.

3.2.5. The bottom type

The special type Nothing, sometimes called the bottom type, represents:

  • the intersection of all types, or, equivalently

  • the empty set.

Nothing is assignable to all other types, but has no instances.

The type schema for Nothing is empty, that is, it is considered to have no members.

Nothing is considered to belong to the module ceylon.language. However, it cannot be defined within the language.

Note: an expression of type Nothing results in a compiler warning.

Because of the restrictions imposed by Ceylon's mixin inheritance model:

  • If X and Y are classes, and X is not a subclass of Y, and Y is not a subclass of X, then the intersection type X&Y is equivalent to Nothing.

  • If X is an interface, the intersection type X&Null is equivalent to Nothing.

  • If X is an interface, and Y is a final class, and Y is not a subtype of X, then the intersection type X&Y is equivalent to Nothing.

  • If X<T> is invariant in its type parameter T, and the distinct types A and B do not involve type parameters, then X<A>&X<B> is equivalent to Nothing.

  • If X is a subtype of a type A and Y is a subtype of a type B, where A and B are distinct cases of an enumerated type, then the intersection type X&Y is equivalent to Nothing.

Furthermore, as a special case,

  • Sequence<E> is equivalent to Nothing if E is equivalent to Nothing, and

  • Tuple<E,F,R> is equivalent to Nothing if any of E, F, or R is equivalent to Nothing.

Note: the soundness of these rules is guaranteed by the implementations of the sealed types Sequence and Tuple in the module ceylon.language.

3.2.6. Principal typing

An expression, as defined in Chapter 6, Expressions, occurring at a certain location, may be assignable to a type. In this case, every evaluation of the expression at runtime produces an instance of a class that is a subtype of the type, or results in a thrown exception, as defined in Chapter 8, Execution.

Given an expression occurring at a certain location, a type T is the principal type of the expression if, given any type U to which the expression is assignable, T is a subtype of U. Thus, the principal type is the "most precise" type for the expression. The type system guarantees that every expression has a principal type. Thus, we refer uniquely to the type of an expression, meaning its principal type at the location at which it occurs.

3.2.7. Type expressions

Function and value declarations usually declare a type, by specifying a type expression.

Type: UnionType | EntryType

Type expressions are formed by combining types using union, intersection, and type abbreviations.

Type expressions support grouping using angle brackets:

GroupedType: "<" Type ">"

Applied types are identified by the name of the type (a class, interface, type alias, or type parameter), together with a list of type arguments if the type declaration is generic.

TypeNameWithArguments: TypeName TypeArguments?

Type names are resolved to type declarations according to §5.1.7 Unqualified reference resolution and §5.1.8 Qualified reference resolution.

If the type is a class, interface, or type alias nested inside a containing class or interface, the type must be fully qualified by its containing types, except when used inside the body of a containing type.

BaseType: PackageQualifier? TypeNameWithArguments | GroupedType
QualifiedType: BaseType ("." TypeNameWithArguments)*

If a type declaration is generic, a type argument list must be specified. If a type declaration is not generic, no type argument list may be specified.

A base type may be qualified by the package keyword, allowing disambiguation of the type name, as defined in §5.1.7 Unqualified reference resolution.

PackageQualifier: "package" "."

Note: the name of a type may not be qualified by its package name. Alias imports, as defined in §4.2.4 Alias imports may be used to disambiguate type names.

BufferedReader.Buffer
Entry<Integer,Element>

3.2.8. Type abbreviations

Certain important types may be written using an abbreviated syntax.

PrimaryType: AtomicType | OptionalType | SequenceType | CallableType
AtomicType: QualifiedType | EmptyType | TupleType | IterableType

First, there are postfix-style abbreviations for optional types and sequence types.

OptionalType: PrimaryType "?"
SequenceType: PrimaryType "[" "]"

For any type X:

  • X? means Null|X, and

  • X[] means Sequential<X>.

Note: the type expression X? is pronounced as “maybe x”, and X[] as “sequence of x”.

Next, there are type abbreviations for callable types which represent the types of functions.

CallableType: PrimaryType "(" (TypeList? | SpreadType) ")"
TypeList: (DefaultedType ",")* (DefaultedType | VariadicType)
DefaultedType: Type "="?
VariadicType: UnionType ("*" | "+")
SpreadType: "*" UnionType

For any type X:

  • X(Y,Z) means Callable<X,[Y,Z]> where Y,Z is a list of types of any length, and

  • X(*Y) means Callable<X,Y> for any subtype Y of Sequential<Anything>.

More precisely, the type meant by a callable type abbreviation is Callable<X,T> where X is the type outside the parentheses in the the callable type abbreviation, and T is the tuple type formed by the types listed inside the parentheses.

Next, abbreviations for iterable types are written using braces.

IterableType: "{" UnionType ("*"|"+") "}"

For any type X:

  • {X*} means Iterable<X,Null>, and

  • {X+} means Iterable<X,Nothing>.

Note: the type expression {X*} is pronounced as “stream of x”, and {X+} as “nonempty stream of x”.

Next, abbreviations for sequence types and tuple types may be written using brackets.

EmptyType: "[" "]"
TupleType: "[" TypeList "]" | PrimaryType "[" DecimalLiteral "]"
  • [] means Empty,

  • [X] means Tuple<X,X,[]> for any type X,

  • [X=] means []|[X] for any type X,

  • [X*] means Sequential<X> for any type X,

  • [X+] means Sequence<X> for any type X,

  • [X,Y] means Tuple<X|Y,X,[Y]> for any types X,Y,

  • [X,Y=] means Tuple<X|Y,X,[Y=]> for any types X,Y,

  • [X,Y*] means Tuple<X|Y,X,[Y*]> for any types X,Y,

  • [X,Y+] means Tuple<X|Y,X,[Y+]> for any types X,Y, and, finally,

  • X[1] means [X], for any type X, and X[n] means Tuple<X,X,X[n-1]> for any type X and positive integer n.

More precisely:

  • A tuple type abbreviation of form [X, ... ] means the type Tuple<X|Y,X,T> where T is the type meant by the type abbreviation formed by removing the first element type X from the list of types in the original tuple type abbreviation, and T has the principal instantiation Y[], as defined in §3.7 Principal instantiations and polymorphism.

  • A tuple type abbreviation of form [X=, ... ] means the type Empty|T where T is the type meant by the tuple type abbreviation [X, ... ], formed by removing the = from the first element type X= of the list of types in the original tuple type abbreviation.

In a tuple type or callable type expression:

  • an defaulted element is indicated with a postfix = or *, and

  • a required element is indicated with a postfix + or no special marker.

In a tuple type or callable type expression, every defaulted element must occur after every required element.

Finally, an entry type may be abbreviated using an arrow.

EntryType: UnionType "->" UnionType
  • X->Y means Entry<X,Y>, for any types X, Y.

Note: the abbreviations T[] and [T*] are synonyms. The syntax T[] is supported for reasons of nostalgia.

Abbreviations may be combined:

String?[] words = { "hello", "world", null };
String? firstWord = words[0];

String->[Integer,Integer] onetwo = "onetwo"->[1, 2];

[Float+](Float x, Float[] xs) add = (Float x, Float[] xs) => [x, *xs];

When a type appears in a value expression, these abbreviations cannot be used (they cannot be disambiguated from operator expressions).

3.2.9. Type inference

Certain declarations which usually require an explicit type may omit the type, forcing the compiler to infer it, by specifying the keyword value, as defined in §4.8.4 Value type inference, or function, as defined in §4.7.4 Function return type inference, where the type usually appears.

value names = people*.name;
function parse(String text) => text.split(" .!?,:;()\n\f\r\t".contains);

Type inference is only allowed for declarations which are referred to only by statements and declarations that occur within the lexical scope of the declaration, as specified by §5.1.6 Type inference and block structure. A value or function declaration may not:

Nor may a parameter or forward-declared value, as defined in §4.8.5 Forward declaration of values, or of a forward-declared function, as defined in §4.7.5 Forward declaration of functions, have an inferred type.

These restrictions allow the compiler to infer undeclared types in a single pass of the code.

Note: in future releases of the language, the inferred type will be context-dependent, that is, in program elements immediately following an assignment or specification, the inferred type will be the type just assigned. When conditional execution results in definite assignment, the inferred type will be the union of the conditionally assigned types. This will allow us to to relax the restriction that forward-declared functions and values can't have their type inferred. For example:

value one;
if (float) {
    one = 1.0;
    Float float = one;
}
else {
    one = 1;
    Integer int = one;
}
Float|Integer num = one;

An inferred type never involves an anonymous class, as defined in §4.5.7 Anonymous classes. When an inferred type would involve an anonymous class type, the anonymous class is replaced by the intersection of the class type it extends with all interface types it satisfies.

TODO: properly define how expressions with no type occurring in a dynamic block affect type inference.

3.2.10. Type alias elimination

A type alias is a synonym for another type. A generic type alias is a type constructor that produces a type alias, given a list of type arguments.

Every type alias must be reducible to an equivalent type that does not involve any type aliases by recursive replacement of type aliases with the types they alias. Thus, circular type alias definitions, as in the following example, are illegal:

alias X => List<Y>;  //error: circular type alias definition
alias Y => List<X>;  //error: circular type alias definition

Replacement of type aliases with the types they alias occurs at compile time, so type aliases are not reified types, as specified in §8.1.2 Type argument reification.

3.3. Inheritance

Inheritance is a static relationship between classes, interfaces, and type parameters:

We say that a type declaration X inherits a type declaration Y if X extends or satisfies Y, or if a third type declaration Z inherits Y and X extends or satisfies Z.

Inheritance relationships may not produce cycles, since that would violate the noncircularity rule for subtyping. Thus, a class, interface, or type parameter may not, directly or indirectly, inherit itself.

When a type declaration extends or satisfies a parameterized type declaration, it must specify type arguments for the type parameters of the generic declaration. Thus, whenever a type declaration inherits a parameterized type declaration, it also inherits an instantiation of the parameterized type declaration.

Note: when a type declaration specifies a relationship to other types, Ceylon visually distinguishes between a list of types which conceptually represents a combination of (intersection of) the types, and a list of types which represents a choice between (union of) the types. For example, when a class C satisfies multiple interfaces, they are written as X&Y&Z. On the other hand, the cases of an enumerated class E are written as X|Y|Z. This syntax emphasizes that C is also a subtype of the intersection type X&Y&Z, and that E may be narrowed to the union type X|Y|Z using a switch statement or the of operator.

3.3.1. Inheritance and subtyping

Inheritance relationships between classes, interfaces, and type parameters result in subtyping relationships between types.

  • If a type declaration X with no type parameters inherits a type Y, then X is a subtype of Y.

  • If a generic type X inherits a type Y, which might involve the type parameters of X, then for any instantiation U of X we can construct a type V by, for every type parameter T of X, substituting the corresponding type argument of T given in U everywhere T occurs in Y, and then U is a subtype of V.

3.3.2. Extension

A class may extend another class, in which case the first class is a subtype of the second class and inherits its members. A class which extends another class may have a constructor, as defined in §4.9 Constructors, which delegates to a callable constructor of the second class. Extension and constructor delegation is specified using the extends clause.

The extends clause must specify exactly one class or constructor.

ExtendedType: "extends" (Extension | Construction)

An extends clause of a class or constructor has either:

  • a reference to a superclass, followed by an optional positional argument list, as defined in §6.6.7 Positional argument lists, or

  • a reference to a superclass constructor, always followed by a positional argument list.

In the case that the extends clause refers to a constructor, the superclass is taken to be the class to which the constructor belongs.

Extension: (BaseExtension | SuperExtension) PositionalArguments?
Construction: (BaseConstruction | SuperConstruction) PositionalArguments

The extends clause may not refer to a partial constructor of the superclass, nor to a value constructor of the superclass.

BaseExtension: PackageQualifier? TypeNameWithArguments
SuperExtension: SuperQualifier TypeNameWithArguments
BaseConstruction: (PackageQualifier? TypeNameWithArguments ".")? MemberNameWithArguments
SuperConstruction: SuperQualifier MemberNameWithArguments
SuperQualifier: "super" "."

The specification of the superclass or superclass constructor is treated as a value expression, not as a type expression.

The type of the value expression is the inherited type.

The specification of the superclass or superclass constructor may have type arguments, and, additionally, the extends clause may have a positional argument list:

  • If the superclass is a parameterized type, the extends clause must also explicitly specify type arguments, and the resulting applied type is inherited.

  • If the extends clause belongs to a constructor or to a class with an initializer parameter list, the extends clause must specify arguments for the initializer parameters of the superclass or parameters of the superclass constructor.

  • If the extends clause belongs to a class with no initializer parameter list, the extends clause may not specify arguments for the initializer parameters of the superclass, and the extends clause may not refer to a constructor.

The type arguments may not be inferred from the positional arguments.

A type argument occurring in the extends clause may not involve variance annotations in or out, defined below in §3.6.1 Type arguments and variance.

extends Singleton<String>("")
extends Person(name, org)
extends withName(name)

A member class annotated actual may use the qualifier super in the extends clause to refer to the member class it refines. When the qualifier super appears, the following class name refers to a member class of the superclass of the class that contains the member class annotated actual.

extends super.Buffer()

The root class Anything defined in ceylon.language does not have a superclass.

3.3.3. Satisfaction

The satisfies clause does double duty. It's used to specify that a class or interface is a direct subtype of one or more interfaces, and to specify upper bound type constraints applying to a type parameter.

Note: for this reason the keyword is not named "implements". It can't reasonably be said that a type parameter "implements" its upper bounds. Nor can it be reasonably said that an interface "implements" its super-interfaces.

  • A class or interface may satisfy one or more interfaces, in which case the class or interface is a subtype of the satisfied interfaces, and inherits their members.

  • A type parameter may satisfy one or more interfaces, optionally, a class, and optionally, another type parameter. In this case, the satisfied types are interpreted as upper bound type constraints on arguments to the type parameter.

Note: currently, a type parameter upper bound may not be specified in combination with other upper bounds. This restriction will likely be removed in future.

The satisfies clause may specify multiple types.

SatisfiedTypes: "satisfies" PrimaryType ("&" PrimaryType)*

If a satisfied class or interface is a parameterized type, the satisfies clause must explicitly specify type arguments, and the resulting applied type is inherited.

A type occurring in the satisfies clause may not involve variance annotations in or out, defined below in §3.6.1 Type arguments and variance.

satisfies Correspondence<Integer,Element> & Collection<Element>

A satisfies clause may not contain two instantiations of the same type declaration.

3.4. Case enumeration and coverage

Coverage is a static relationship between classes, interfaces, and type parameters, produced through the use of case enumeration:

  • An abstract class or interface may be an enumerated type, with an enumerated list of disjoint subtypes called cases, as defined by §4.5.8 Enumerated classes and §4.4.4 Enumerated interfaces.

  • A type parameter may have an enumerated bound, with an enumerated list possible type arguments, as defined by §3.5.3 Generic type constraints.

  • An abstract class or interface may have a self type, a type parameter representing the concrete type of an instance.

3.4.1. Coverage

Coverage is a strictly weaker relationship than assignability:

  • If a type is a subtype of a second type, then the second type covers the first type.

  • If a type has a self type, then its self type covers the type.

  • If a type X enumerates its cases X1, X2, etc, then the union X1|X2|... of its cases covers the type.

  • If a generic type X enumerates its cases, X1, X2, etc, which might involve the type parameters of X, then for any instantiation U of X, and for each case Xi, we can construct a type Ui by, for every type parameter T of X, substituting the corresponding type argument of T given in U everywhere T occurs in Xi, and then the union type U1|U2|... of all the resulting types Ui covers Y.

  • If a type X covers two types A and B, then X also covers their union A|B.

  • If X and Y are both instantiations of a generic type G, and if the type Z is formed by replacing every covariant argument in Y with the intersection of the upper bounds of the corresponding type parameter of G, after substitution of the given type arguments in Y for any occurrences of the type parameters of G in the upper bounds, except where the argument is already a subtype of the upper bounds, then if X covers Z, then X also covers Y.

  • Coverage is transitive. If X covers Y and Y covers Z, then X covers Z.

It follows that coverage obeys the identity property of assignability: a type covers itself. However, coverage does not obey the noncircularity property of assignability. It is possible to have distinct types A and B where A covers B and B covers A.

Case enumeration allows safe use of a type in a switch statement, or as the subject of the of operator. The compiler is able to statically validate that the switch contains an exhaustive list of all cases of the type, by checking that the union of cases enumerated in the switch covers the type, or that the second operand of of covers the type.

Note: however, a type is not considered automatically assignable to the union of its cases, or to its self type. Instead, the type must be explicitly narrowed to the union of its cases, nor to its self type, using either the of operator or the switch construct. This narrowing type conversion can be statically checked—if X covers Y then Y of X is guaranteed to succeed at runtime. Unfortunately, and quite unintuitively, the compiler is not able to analyse coverage implicitly at the same time as assignability, because that results in undecidability!

3.4.2. Cases

The of clause does triple duty. It's used to define self types and type families, enumerated types, and enumerated type constraints. The of clause may specify multiple elements, called cases.

CaseTypes: "of" CaseType ("|" CaseType)*
CaseType: ValueCase | PrimaryType
ValueCase: ("package" ".")? MemberName

A type occurring in the of clause may not involve variance annotations in or out, defined below in §3.6.1 Type arguments and variance.

If an interface or abstract class with an of clause has exactly one case, and it is a type parameter of the interface or abstract class, or of the immediately containing type, if any, then that type parameter is a self type of the interface or abstract class, and:

  • the self type parameter covers the declared type within the body of the declaration,

  • the type argument to the self type parameter in an instantiation of the declared type covers the instantiation, and

  • every type which extends or satisfies an instantiation of the declared type must also be covered by the type argument to the self type parameter in the instantiation.

shared abstract class Comparable<Other>() of Other 
        given Other satisfies Comparable<Other> {
    
    shared formal Integer compare(Other that);
    
    shared Integer reverseCompare(Other that) 
            => that.compare(this) of Other;
    
}
Comparable<Item> comp = ... ;
Item item = comp of Item;

Otherwise, an interface or abstract class with an of clause may have multiple cases, but each case must be either:

  • a subtype of the interface or abstract class, or

  • a value reference to a toplevel anonymous class, as defined in §4.5.7 Anonymous classes, that is a subtype of the interface or abstract class.

Then the interface or abstract class is an enumerated type, and every subtype of the interface or abstract class must be a subtype of exactly one of the enumerated subtypes. A class or interface may not be a subtype of more than one case of an enumerated type.

If a concrete class has an of clause, then each case must be a value reference to a value constructor of the class, as defined in §4.9 Constructors, and the class must be a toplevel class. Then the concrete class is an enumerated type, and there may be no additional non-partial constructors of the class that are not listed in the of clause.

of larger | smaller | equal
of Root<Element> | Leaf<Element> | Branch<Element>

A type parameter with an of clause may specify multiple cases, as defined in §3.5.3 Generic type constraints.

An of clause may not contain:

  • two instantiations of the same type declaration, or

  • two value references to the same toplevel anonymous class or value constructor.

3.4.3. Generic enumerated types

If a generic enumerated type X has a case type C, then C must directly extend or satisfy an instantiation Y of X, and for each type parameter T of X and corresponding argument A of T given in Y, either:

  • X is covariant in T and A is exactly Nothing,

  • X is contravariant in T and A is exactly the intersection of all upper bounds on T, or Anything if T has no upper bounds, or

  • C is an instantiation of a generic type G and A is exactly S for some type parameter S of G, and S must have the same variance as T.

Furthermore, if C is an instantiation of a generic type, then T may not occur twice in C.

For example, the following covariant enumerated type is legal:

interface List<out Element> 
        of Cons<Element> | nil { ... }

class Cons<out Element>(Element element) 
        satisfies List<Element> { ... }

object nil 
        satisfies List<Nothing> { ... }

As is the following contravariant enumerated type:

interface Consumer<in Event> 
        of Logger | Handler<Event> 
        given Event satisfies AbstractEvent { ... }

interface Logger 
        satisfies Consumer<AbstractEvent> { ... }

interface Handler<in Event> 
        satisfies Consumer<AbstractEvent> 
        given Event satisfies AbstractEvent { ... }

But the following enumerated type is not legal, since it is possible to choose a legal argument T of the type parameter Type of Expression, such that the case types StringLiteral and NumberLiteral aren't subtypes of the instantiation Expression<T>:

interface Expression<out Type>
        of Function<Type> | StringLiteral | NumberLiteral { ... }

interface Function<out Type> 
        satisfies Expression<Type> { ... }

interface StringLiteral
        satisfies Expression<String> { ... } //error String is not exactly Nothing

interface NumberLiteral
        satisfies Expression<Integer|Float> { ... } //error Integer|Float is not exactly Nothing

Note: these rules could be relaxed to allow the definition of generic enumerated types where the list of cases of an instantiation of a generic type depends upon the given type arguments (a "generalized" algebraic type).

3.4.4. Disjoint types

Two types are said to be disjoint if it is impossible to have a value that is an instance of both types. If X and Y are disjoint, then their intersection X&Y is the bottom type Nothing.

Two types X and Y are disjoint if either:

  • X is a subtype of a type A and Y is a subtype of a type B, where A and B are distinct cases of an enumerated type,

  • X and Y are both classes and X is not a subclass of Y and Y is not a subclass of X,

  • X is the class Null and Y is an interface,

  • X is an anonymous class or an instantiation of a final class and Y is an instantiation of a class of interface, and X does not inherit Y,

  • X is an anonymous class or a final class with no type parameters and Y is a type in which no type parameter reference occurs, and X is not a suptype of Y,

  • X is a type parameter and Y and the intersection of the upper bounds of X are disjoint,

  • X is a union type A|B and both Y and A are disjoint and Y and B are disjoint,

  • X is an enumerated type with cases A1|A2|... and for every case Ai of X, Y and Ai are disjoint,

  • X is an intersection type A&B and either Y and A are disjoint or Y and B are disjoint, or

  • X and Y inherit disjoint instantiations of a generic type Z, that is, two instantiations of Z that have the intersection Nothing, as defined below, in §3.7.3 Principal instantiation inheritance.

Furthermore, as a special case, the types X and Y are disjoint if:

  • X is a subtype of some instantiation of Sequential, Y is an instantiation of a class or interface that is not a subtype of any instantiation of Sequential, and Y is not an instantiation of a class or interface that is inherited by Sequential,

  • X has the principal supertype instantiation Sequence<A>, Y has the principal supertype instantiation Sequential<B>, and A and B are disjoint,

  • X has the principal supertype instantiation Sequential<A>, Y has the principal supertype instantiation Tuple<J,B,V>, and A and B are disjoint or Sequential<A> and V are disjoint, or

  • X has the principal supertype instantiation Tuple<I,A,U>, Y has the principal supertype instantiation Tuple<J,B,V>, and A and B are disjoint or U and V are disjoint.

Note: the soundness of these rules is guaranteed by the implementations of the sealed types Sequence, Sequential, Range, and Tuple in the module ceylon.language.

3.5. Generic type parameters

A function, class, or interface schema may be parameterized by one or more generic type parameters. A parameterized type schema defines a type constructor, a function that produces a type given a tuple of compatible type arguments. A parameterized class or function schema defines a function that produces the signature of an invokable operation given a tuple of compatible type arguments.

TypeParameters: "<" (TypeParameter ",")* TypeParameter ">"

A declaration with type parameters is called generic or parameterized.

  • A type schema with no type parameters defines exactly one type. A parameterized type schema defines a template for producing types: one type for each possible combination of type arguments that satisfy the type constraints specified by the type. The types of members of the this type are determined by replacing every appearance of each type parameter in the schema of the parameterized type definition with its type argument.

  • A function schema with no type parameters defines exactly one operation per type. A parameterized function declaration defines a template for producing overloaded operations: one operation for each possible combination of type arguments that satisfy the type constraints specified by the method declaration.

  • A class schema with no type parameters defines exactly one instantiation operation. A parameterized class schema defines a template for producing overloaded instantiation operations: one instantiation operation for each possible combination of type arguments that satisfy the type constraints specified by the class declaration. The type of the object produced by an instantiation operation is determined by substituting the same combination of type arguments for the type parameters of the parameterized class schema.

Note: by convention, type parameter names should be constructed from meaningful words. The use of single-letter type parameter names is discouraged. The name of a type parameter should be chosen so that declarations within the body of the parameterized declaration read naturally. For example, class Entry<Key,Item> is reasonable, since Key key and Item item read naturally within the body of the Entry class. The following identifier names usually refer to a type parameter: Element, Other, This, Value, Key, Item, Absent, Argument, Args and Result. Avoid, where reasonable, using these names for interfaces and classes.

3.5.1. Type parameters and variance

A type parameter allows a declaration to be abstracted over a constrained set of types.

TypeParameter: Variance TypeName ("=" Type)?

Every type parameter has a name and a variance.

Variance: ("out" | "in")?
  • A covariant type parameter is indicated using the keyword out.

  • A contravariant type parameter is indicated using the keyword in.

  • By default, a type parameter is invariant.

A type parameter may, optionally, have a default type argument. A type parameter with a default type argument must occur after every type parameter with no default type argument in the type parameter list.

The default type argument for a type parameter must satisfy the constraints on the type parameter.

TODO: this restriction could be relaxed, and the assignability of the default type argument to the type constraints checked at use-sites where the default type argument is used in type expressions.

A default type argument expression for a type parameter of a generic declaration may not involve:

  • the type parameter itself,

  • any type parameter of the declaration that occurs later in the list of type parameters, nor

  • the generic declaration.

Within the body of the schema it parameterizes, a type parameter is itself a type. The type parameter is a subtype of every upper bound of the type parameter. However, a class or interface may not extend or satisfy a type parameter.

<Key, out Item>
<in Message>
<out Element=Object>
<in Left, in Right, out Result>

3.5.2. Variance validation

A covariant type parameter may only appear in covariant positions of the parameterized schema. A contravariant type parameter may only appear in contravariant positions of the parameterized schema. An invariant type parameter may appear in any position.

Furthermore, a type with a contravariant type parameter may only appear in a covariant position in an extended type, satisfied type, case type, or upper bound type constraint.

Note: this restriction exists to eliminate certain undecidable cases described in the paper Taming Wildcards in Java's Type System, by Tate et al.

To determine if a type expression occurs in a covariant or contravariant position, we first consider how the type occurs syntactically.

For a generic function we examine the return type of the function, which is a covariant position.

For a generic type schema we examine each shared member, along with extended/satisfied types and case types.

Note: since the visibility rules are purely lexical in nature, it is legal for a member expression occurring in the body of a class or interface to have a receiver expression other that is not a self-reference, as defined in §6.3 Self references, and refer to an un-shared member of the class or interface. In this special case, the member is treated as if it were shared for the purposes of the following variance validation rules.

  • An extended type, satisfied type, or case type of the type schema itself is a covariant position.

In a shared method declaration of the parameterized type schema:

  • The return type of the method is a covariant position.

  • Any parameter type of the method is a contravariant position.

  • Any upper bound or enumerated bound of a type parameter of the method is a contravariant position.

In a shared attribute declaration that is neither variable nor late:

  • The type of the attribute is a covariant position.

In a shared reference declaration that is either variable or late:

  • The type of the attribute is an invariant position.

In a shared nested class declaration of the parameterized type schema:

  • Any initializer parameter type of the class is a contravariant position.

  • Any callable constructor parameter type of the class is an invariant position of the class itself, but a contravariant position of any outer containing type.

  • Any upper bound or enumerated bound of a type parameter of the class is a contravariant position.

  • An extended type, satisfied type, or case type of the nested class is a covariant position.

  • Every covariant position of the nested class schema is a covariant position of the containing type schema. Every contravariant position of the nested class schema is a contravariant position of the containing type schema.

In a shared nested interface declaration of the parameterized type schema:

  • An extended type, satisfied type, or case type of the nested interface is a covariant position.

  • Every covariant position of the nested interface schema is a covariant position of the containing type schema. Every contravariant position of the nested interface schema is a contravariant position of the containing type schema.

For parameters of callable parameters, we first determine if the callable parameter itself is covariant or contravariant:

  • A callable parameter of a method or nested class is contravariant.

  • A callable parameter of a covariant parameter is contravariant.

  • A callable parameter of a contravariant parameter is covariant.

Then:

  • The return type of a covariant callable parameter is a covariant position.

  • The return type of a contravariant callable parameter is a contravariant position.

  • The type of a parameter of a covariant callable parameter is a contravariant position.

  • The type of a parameter of a contravariant callable parameter is a covariant position.

Finally, to determine if a type parameter that occurs as a type argument occurs in a covariant or contravariant position, we must consider the declared variance of the corresponding type parameter:

  • A type argument of a covariant type parameter of a type in a covariant position is a covariant position.

  • A type argument of a contravariant type parameter of a type in a covariant position is a contravariant position.

  • A type argument of a covariant type parameter of a type in a contravariant position is a contravariant position.

  • A type argument of a contravariant type parameter of a type in a contravariant position is a covariant position.

  • A type argument of an invariant type parameter of a type in any position is an invariant position.

  • A type argument of any type parameter of a type in an invariant position is an invariant position.

3.5.3. Generic type constraints

A parameterized method, class, or interface declaration may declare constraints upon ordinary type parameters using the given clause.

TypeConstraints: TypeConstraint+

There may be at most one given clause per type parameter.

TypeConstraint: "given" TypeName TypeConstraintInheritance
TypeConstraintInheritance: CaseTypes? SatisfiedTypes?

Note that the syntax for a type constraint is essentially the same syntax used for other type declarations such as class and interface declarations.

There are two different kinds of type constraint:

  • An upper bound, given X satisfies T, specifies that the type parameter X is a subtype of a given type T.

  • An enumerated bound, given X of T|U|V specifies that the type parameter X represents one of the enumerated types.

The types listed in an enumerated bound must be mutually disjoint, and each type must be a class or interface type.

TODO: Should we allow unions in upper bounds? Should we allow intersections in enumerated bounds?

A single given clause may specify multiple constraints on a certain type parameter. In particular, it may specify multiple upper bounds together with an enumerated bound. If multiple upper bounds are specified, at most one upper bound may be a class, and at most one upper bound may be a type parameter.

Note: in Ceylon 1.0, a type parameter with multiple upper bounds may not have an upper bound which is another type parameter.

given Value satisfies Ordinal<Value> & Comparable<Value>
given Argument of String | Integer | Float

A type parameter is a subtype of its upper bounds.

class Holder<Value>(shared Value element) 
        extends Object()
        given Value satisfies Object {
    shared actual Boolean equals(Object that) {
        return if (is Holder<Value> that
            then element==that.element
            else false;
    }
    shared actual Integer hash => element.hash;
}

Every type parameter has an implicit upper bound of type Anything.

TODO: eventually, we would like to have Ceylon's system of flow-sensitive typing support a special sort ofswitch over the cases of a type parameter with an enumerated bound:

Characters uppercase<Characters>(Characters chars) 
       given Characters of String | Range<Character> { 
    switch (Characters)
    case (satisfies String) { 
        return chars.uppercased;
    }
    case (satisfies Range<Character>) { 
        return chars.first.uppercased..chars.last.uppercased;
    }
}

Note: we have often searched for a need for lower bound type constraints. The syntax would be:

given T abstracts One|Two

With union types they don't appear to be very useful, since it seems that almost every operation with a lower bound can be rewritten in a more general form using a union type. However, perhaps lower bounds will someday turn out to be useful when combined with contravariant types. (A lower bound on a parameter which occurs as the argument of a contravariant type is more like an upper bound).

Note: since we have reified types, it would be possible to support a type constraint that allows instantiation of the type parameter.

given T(Object arg)

The problem with this is that then inferring T is fragile. And if we don't let it be inferred, we may as well pass T as an ordinary parameter. So Ceylon, unlike C#, doesn't support this.

3.6. Generic type arguments

A list of type arguments produces a new type schema from a parameterized type schema, or a new function schema from a from a parameterized function schema. In the case of a type schema, this new schema is the schema of an applied type, and is called an instantiation of the parameterized type schema.

A type argument list is a list of type arguments.

TypeArguments: "<" ((TypeArgument ",")* TypeArgument)? ">"

A type argument is a type with a variance.

TypeArgument: Variance Type

A type argument may itself be an applied type, or type parameter, or may involve unions and intersections.

<Key, List<Item>>
<String, Person?>
<String[](Integer), [{Object*}]>
<out Object, in Nothing>

Type arguments are assigned to type parameters according to the positions they occur in the list.

3.6.1. Type arguments and variance

Every type argument has a variance:

  • if the type argument is annotated out then it must be assigned to an invariant type parameter, and it is covariant,

  • if the type argument is annotated in then it must be assigned to an invariant type parameter, and it is contravariant, or,

  • otherwise, the type argument has the same variance as the type parameter to which it is assigned.

It is illegal for both the type parameter and its type argument to have an explicit variance.

3.6.2. Type argument substitution

Given the schema of a generic declaration, we form the new schema by type argument substitution. Each type argument is substituted for every appearance of the corresponding type parameter in the schema of the generic declaration, including:

  • attribute types,

  • function or method return types,

  • function or method parameter types,

  • class initializer and callable constructor parameter types, and

  • type arguments of extended classes and satisfied interfaces.

When a type argument A with no explicit variance annotation is substituted for a type parameter T, all occurrences of T in the schema of the generic declaration are replaced with A.

For type arguments with explicit variance of a type parameter T, substitution of the type argument depends upon whether an occurrence of T is a covariant or contravariant position in the schema of the generic declaration, as defined above in §3.5.2 Variance validation.

When a type argument out A explicitly marked covariant is substituted for a type parameter T:

  • Every occurrence of T in a covariant position as a type argument of an invariant type parameter is replaced by out A.

  • Every other occurrence of T in a covariant position is replaced by A.

  • Every occurrence of T in a contravariant position is replaced by Nothing.

  • Every applied type expression E involving A, and occurring as a type argument of an invariant type parameter, and which was replaced by F according to the previous rules is replaced by out F.

When a type argument in A explicitly marked contravariant is substituted for a type parameter T:

  • Every occurrence of T in a contravariant position as a type argument of an invariant type parameter is replaced by in A.

  • Every other occurrence of T in a contravariant position is replaced by A.

  • Every occurrence of T in a covariant position is replaced by the intersection of the upper bound type constraints on T in which T itself does not occur covariantly, or by Anything if there are no such constraints.

  • Every applied type expression E involving A, and occurring as a type argument of an invariant type parameter, and which was replaced by F according to the previous rules is replaced by out F.

3.6.3. Type arguments and type constraints

A generic type constraint affects the type arguments that can be assigned to a type parameter in any type argument list belonging directly to:

  • a base expression or member expression

  • an applied type expression that occurs directly in a satisfies, of, or extends clause, or

  • a metamodel expression, as defined by §6.9 Metamodel expressions.

A type constraint does not apply to any type argument list belonging to an applied type expression that occurs:

  • outside of the satisfies, of, and extends clauses, or

  • as a type argument within these clauses.

In locations where type constraints apply:

  • A type argument to a type parameter T with an upper bound must be a type which is a subtype of all upper bounds of T in the realization of the generic declaration, as defined in §3.7.7 Realizations.

  • A type argument to a type parameter T with an enumerated bound must be a subtype of one of the enumerated types of the bound on T in the realization of the generic declaration, or it must be a type parameter A with an enumerated bound where every enumerated type of the bound on A is a subtype of one of the enumerated types of the bound on T in the realization of the generic declaration.

A type argument list conforms to a type parameter list if, for every type parameter in the list, either:

  • there is a type argument to the type parameter, and either the type argument satisfies the constraints of the type parameter, or the type argument list occurs in a location where type constraints do not apply, or, alternatively,

  • there is no explicit type argument but the type parameter has a default type argument, in which case the type argument is defaulted by substituting the arguments of all type parameters that occur earlier in the list of type parameters of the declaration into this default type argument.

There must be at least as many type parameters as type arguments. There must be at least as many type arguments as type parameters without default values.

3.6.4. Applied types and and variance

If a type argument list conforms to a type parameter list, the combination of the parameterized type together with the type argument list is itself a type, called an applied type. We also call the applied type an instantiation of the generic type.

For a generic type X, the instantiations Y and Z of X represent the same type if and only if for every type parameter P of X and corresponding type arguments A in Y and B in Z:

  • A is exactly the same type as B, and the variance of A is the same as B,

  • A and B are both covariant type arguments, and both types are supertypes of P,

  • either A or B is a contravariant type argument with type precisely Nothing, and the other type argument is covariant and its type is a supertype of P,

  • both A and B have type precisely Nothing, and one is an invariant type argument, and the other is a covariant type argument, or

  • both A and B have types which are supertypes of P, and one is an invariant type argument, and the other is an contravariant type argument.

For a generic type G, and instantiations Y and Z of G, Y is a subtype of Z if and only if, for every type parameter T of G, and corresponding arguments A specified in Y and B specified in Z:

  • B is a covariant type argument, and T is a subtype of B,

  • B is a contravariant type argument, and the type B is precisely Nothing,

  • B is a covariant type argument, and A is not contravariant, and the type A is a subtype of the type B,

  • B is a contravariant type argument, and A is not covariant, and the type B is a subtype of the type A,

  • B is an invariant type argument, A is a covariant type argument, and T is a subtype of both types, or

  • B is an invariant type argument, A is a contravariant type argument, and both types are precisely Nothing,

  • B and A are both invariant type arguments (neither covariant nor contravariant), and A and B are exactly the same type.

Note that if A is an invariant type argument in the instantiation X<A> of a generic type X<T>, then a type Z is a subtype of X<A> if and only if Z has the principal instantiation X<A>.

3.6.5. Type argument inference

When a direct invocation expression, as defined by §6.6 Invocation expressions, does not explicitly specify type arguments, the type arguments are inferred from the argument expression types.

  • In the case of a direct invocation of a function or class, type arguments are inferred for the type parameters of the function or class.

  • In the case of a direct invocation of a callable constructor, type arguments are inferred for the type parameters of the class to which the constructor belongs.

The types of the argument expressions and the declared types of the corresponding parameters determine an inferred lower bound or inferred upper bound for each type parameter.

If a list of argument expressions has types A1,A2,... and the corresponding list of parameters has declared types P1,P2,... then:

  • The inferred lower bound for a type parameter T of the generic declaration is the conjunction of all inferred lower bounds Ai on Pi for T.

  • The inferred upper bound for a type parameter T of the generic declaration is the conjunction of all inferred upper bounds Ai on Pi for T.

Given types A and P, we determine the inferred lower bound A on P for T according to the nature of A and P:

  • If P is exactly T, and the location at which P occurs in the parameter list is not a contravariant location, the inferred lower bound A on P for T is T abstracts A.

  • If P is a union type Q|R, the lower bound A on P for T is the disjunction of the lower bound A on Q for T with the lower bound A on R for T. Note: this case is special.

  • If P is an intersection type Q&R, the lower bound A on P for T is the conjunction of the lower bound A on Q for T with the lower bound A on R for T.

  • If A is a union type B|C, the lower bound A on P for T is the conjunction of the lower bound B on P for T with the lower bound C on P for T.

  • If A is an intersection type B&C, the lower bound A on P for T is the disjunction of the lower bound B on P for T with the lower bound C on P for T.

  • If P is an applied type Q<P1,P2,...> of a parameterized type Q, and A is a subtype of an applied type Q<A1,A2,..>, the lower bound A on P for T is the conjunction of all lower bounds Ai on Pi for T.

  • Otherwise, if A is not a union or intersection, and if P is neither an applied type, a union, or an intersection, nor exactly T, the lower bound A on P for T is null.

Where:

  • the conjunction of a lower bound T abstracts A with a lower bound T abstracts B is the lower bound T abstracts A|B,

  • the disjunction of a lower bound T abstracts A with a lower bound T abstracts B is the lower bound T abstracts A&B,

  • the conjunction or disjunction of a lower bound T abstracts A with a null lower bound is T abstracts A, and

  • the conjunction or disjunction of two null lower bounds is null.

Given types A and P, we determine the inferred upper bound A on P for T according to the nature of A and P:

  • If P is exactly T, and the location at which P occurs in the parameter list is not a covariant location, the inferred upper bound A on P for T is T satisfies A.

  • If P is a union type Q|R, the upper bound A on P for T is the disjunction of the upper bound A on Q for T with the upper bound A on R for T. Note: this case is special.

  • If P is an intersection type Q&R, the upper bound A on P for T is the conjunction of the upper bound A on Q for T with the upper bound A on R for T.

  • If A is a union type B|C, the upper bound A on P for T is the disjunction of the upper bound B on P for T with the upper bound C on P for T.

  • If A is an intersection type B&C, the upper bound A on P for T is the conjunction of the upper bound B on P for T with the upper bound C on P for T.

  • If P is an applied type Q<P1,P2,...> of a parameterized type Q, and A is a subtype of an applied type Q<A1,A2,..>, the upper bound A on P for T is the conjunction of all upper bounds Ai on Pi for T.

  • Otherwise, if A is not a union or intersection, and if P is neither an applied type, a union, or an intersection, nor exactly T, the upper bound A on P for T is null.

Where:

  • the conjunction of an upper bound T satisfies A with an upper bound T satisfies B is the upper bound T satisfies A&B,

  • the disjunction of an upper bound T satisfies A with an upper bound T satisfies B is the upper bound T satisfies A|B,

  • the conjunction or disjunction of an upper bound T satisfies A with a null upper bound is T satisfies A, and

  • the conjunction or disjunction of two null upper bounds is null.

The inferred type argument to a covariant type parameter T of the generic declaration is:

  • Nothing, if the inferred lower bound for T is null, or, otherwise,

  • the type A, where the inferred lower bound for T is T abstracts A.

The inferred type argument to a contravariant type parameter T of the generic declaration is:

  • Anything, if the inferred upper bound for T is null, or, otherwise,

  • the type A, where the inferred upper bound for T is T satisfies A.

An invariant type parameter T of the generic declaration is treated, for the purposes of type argument inference, as if it were covariant or contravariant, depending upon how it occurs in the types of parameters explicitly assigned arguments by the direct invocation, and, in the case of direct invocation of a generic function or class alias, upon how it occurs in the return type of the function or aliased type of the class alias.

  • If the generic declaration is a function or class alias, and T occurs covariantly in its return type or aliased type, and does not occur contravariantly or invariantly in its return type or aliased type, then T is treated as covariant.

  • If the generic declaration is a function or class alias, and T occurs contravariantly in its return type or aliased type, and does not occur covariantly or invariantly in its return type or aliased type, then T is treated as contravariant.

  • Otherwise, if T occurs contravariantly in the type of any parameter to which an argument is explicity assigned by the argument list of the direct invocation, and does not occur covariantly or invariantly in the type of any parameter to which an argument is explicitly assigned, then T is treated as contravariant.

  • Finally, if none of the above cases apply, T is treated as covariant.

An argument expression with no type occurring in a dynamic block, as defined in §5.3.5 Dynamic blocks, may cause type argument inference to fail. When combining bounds using union, any constituent bound with no type results in a bound with no type. When combining bounds using intersection, any constituent bound with no type is eliminated. If the resulting inferred upper or lower bound has no type, type argument inference is impossible for the type argument, and type arguments must be specified explicitly.

Finally, when every type parameter Pi has been assigned an inferred type argument Ai, each inferred type argument is adjusted according to the upper bound type constraints on Pi. The final inferred type argument is the intersection of Ai with every type Vj formed by substituting all Ais for their corresponding Pis in an upper bound Uj of Pi.

If the inferred type argument does not satisfy the generic type constraints on T, a compilation error results.

Consider the following invocation:

[Element+] prepend<Element>(Element head, Element[] sequence) { ... }
value result = prepend(null, {"hello", "world"});

The inferred type of Element is the union type String?.

Now consider:

class Bag<out Element>(Element* elements) {
    shared Bag<ExtraElement> with<ExtraElement>(ExtraElement* elements) 
            given ExtraElement abstracts Element { ... }
}
Bag<String> bag = Bag("hello", "world");
value biggerBag = bag.with(1, 2, 5.0);

The inferred type of ExtraElement is the union type Integer|Float|String.

Finally consider:

interface Delegate<in Value> { ... }
class Consumer<in Value>(Delegate<Value>* delegates) { ... }
Delegate<String> delegate1 = ... ;
Delegate<Object> delegate2 = ... ; 
value consumer = Consumer(delegate1, delegate2);

The inferred type of Value is Consumer<String>.

TODO: What about upper bounds in which the type parameter itself appears (the infamous self-type problem with Comparable and Numeric) or in which another type parameter appears?

An inferred type argument never involves an anonymous class, as defined in §4.5.7 Anonymous classes. When an inferred type would involve an anonymous class type, the anonymous class is replaced by the intersection of the class type it extends with all interface types it satisfies.

3.7. Principal instantiations and polymorphism

Inheritance interacts with type parameterization to produce subtyping relationships between instantiations of generic types. The notion of an inherited instantiation and the notion of a principal instantation help us reason about these relationships.

Warning: this section is not for the faint of heart. Feel free to skip to Chapter 4, Declarations, unless you're really, really interested in precisely how the compiler reasons about inheritance of generic types.

3.7.1. Inherited instantiations

For a generic type G, inheritance produces subtypes with inherited instantiations of the generic type.

  • If a type X directly extends or satisfies an instantiation V of G, then X has the inherited instantiation V of G.

  • If a generic type H extends or satisfies an instantiation V of G, that may involve the type parameters of H, then for any instantiation U of H, we can construct an instantiation W of G by, for every type parameter T of H, substituting the type argument of T given in U everywhere T occurs in V, and then U has the inherited instantiation W of G.

  • If a type X is a subtype of a type Y, and Y has an inherited instantiation W of a generic type G, then X also has this inherited instantiation.

3.7.2. Type argument distinctness

A pair of type arguments A and B are considered:

  • provably distinct, if neither A nor B involves a type parameter and either:

    • both arguments are invariant, and are not exactly the same type,

    • one argument is covariant and the other argument is invariant and is not a subtype of the covariant argument, or

    • one argument is contravariant and the other argument is invariant and is not a supertype of the contravariant argument,

  • provably not distinct, if either:

    • both arguments are invariant, and are exactly the same type,

    • both arguments are covariant,

    • both arguments are contravariant,

    • one argument is covariant and the other argument is invariant and is a subtype of the covariant argument, or

    • one argument is contravariant and the other argument is invariant and is a supertype of the contravariant argument,

  • otherwise, possibly distinct, if either A or B involves a type parameter and A and B are not provably not distinct, or if A and B have opposite variances.

Note: the unfortunate case of possible distinctness is an incompleteness in the type system arising from the fact that Ceylon does not currently allow a type argument with both an upper and a lower bound, that is, a type argument of form in X out Y.

3.7.3. Principal instantiation inheritance

If a class or interface type X has the inherited instantiations V and W of some generic type Y, then:

  • for every invariant type parameter T of Y, the type argument A of T given in V and the type argument B of T given in W must be exactly the same type, and, furthermore,

  • X is a subtype of an instantiation U of Y such that U is a subtype of V&W.

Therefore, if a type X is a subtype of the instantiations V and W of some generic type Y, then either:

  • for some invariant type parameter T of Y, the argument A of T given in V and the argument B of T given in W are provably distinct type arguments, and then the type V&W is the bottom type Nothing, and we say that V and W are disjoint instantiations of Y, or

  • for some invariant type parameter T of Y, the argument of A of T given in V and the argument B of T given in W are possibly distinct, and then we say that V and W are irreconcilable instantiations of Y, or

  • otherwise, X must be a subtype of an instantiation P of Y formed by taking each type parameter T of Y, and constructing a type argument C for T from the type arguments A of T given in V and B of T given in W:

    • if A and B are both invariant, then they must be exactly the same type, and C is the same type as A and B,

    • if both A and B are covariant, then C is out A&B

    • if both A and B are contravariant, then C is in A|B,

    • if either A or B is covariant and the other is invariant, with exact type D, then C is just D, or

    • if either A or B is contravariant, and the other is invariant, with exact type D, then C is just D.

Finally, the following identities result from principal instantiation inheritance. For any generic type X<T>, and for any given types A and B:

  • X<A>&X<B> is exactly equivalent to X<A&B> if X<T> is covariant in T, unless either A or B involves type parameters, and

  • X<A>&X<B> is exactly equivalent to X<A|B> if X<T> is contravariant in T, unless either A or B involves type parameters.

3.7.4. Principal instantiation of a supertype

If a type X is a subtype of some instantiation V of a generic type Y, then, as a result of the principal instantiation inheritance restriction, we can form a unique instantiation of Y that is a subtype of every instantiation of Y to which X is assignable. We call this type the principal instantiation of Y for X.

We compute principal instantiations by making use of the identities observed above in §3.2.3 Union types, §3.2.4 Intersection types, and §3.7.3 Principal instantiation inheritance. For any generic type X:

  • The principal instantiation of the union U|V of two instantiations of X, U and V, is an instantiation P of X formed by taking each type parameter T of X and constructing a type argument C for T from the type arguments A of T given in U and B of T given in V:

    • if either A or B is covariant, and neither is contravariant, then C is the covariant type argument out A|B,

    • if either A or B is contravariant, and neither is covariant, then C is the contravariant type argument in A&B, or

    • if both A and B are invariant, and if A and B are exactly the same type, then C is this type.

  • The principal instantiation of the intersection U&V of two instantiations of X, U and V, is an instantiation P of X formed by taking each type parameter T of X and constructing a type argument C for T from the type arguments A of T given in U and B of T given in V:

    • if either A or B is covariant, and neither is contravariant, then C is the covariant type argument out A&B,

    • if either A or B is contravariant, and neither is covariant, then C is the contravariant type argument in A|B, or

    • if both A and B are invariant, and if A and B are exactly the same type, then C is this type.

  • Finally, the principal instantiation of a generic type X for a type Y which has one or more inherited instantiations of X is the principal instantiation of the intersection of all the inherited instantiations of X.

Note: since we do not support type arguments with both upper and lower bounds, there are two cases where we cannot form a principal instantiation for an intersection type.

  • Intersections such as X<in A> & X<out B>, where the principal instantiation would be X<in A out B>.

  • An intersection X<A> & X<P> of two instantiations of an invariant type, X<T> where one type argument P is a type parameter. The principal instantiation should be X<in A|P out A&P>.

In these cases we simply disallow references to members of the intersection type.

3.7.5. Refinement

A class or interface may declare an actual member with the same name as a member that it inherits from a supertype if the supertype member is declared formal or default. Then we say that the first member refines the second member, and it must obey restrictions defined in §4.5.6 Member class refinement, §4.7.8 Method refinement, or §4.8.7 Attribute refinement.

A declaration may not be annotated both formal and default.

If a declaration is annotated formal, default, or actual then it must also be annotated shared.

For any class or interface X, and for every declared or inherited member of X that is not refined by some other declared or inherited member of X, and for every other member declared or inherited by X that directly or indirectly refines a declaration that the first member itself directly or indirectly refines, the principal instantiation for X of the type that declares the first member must be a subtype of the principal instantiation for X of the type that declares the second member.

Note: a related restriction is defined in §5.1.1 Declaration name uniqueness.

3.7.6. Qualified types

A type declaration that directly occurs in the body of another type is called a nested type. If a nested type is annotated shared, it may be used in a type expression outside the body in which it is declared, if and only if it occurs as a qualified type, as specified in §3.2.7 Type expressions.

The qualified types X.U and Y.V are exactly the same types if and only if U is exactly the same type as V, and in the case that this type is a member of a generic type Z, then the principal instantiation of Z for X is exactly the same type as the principal instantiation of Z for Y.

A qualified type X.U is a subtype of a qualified type Y.V if U is a subtype of V, and in the case that V is a member of a generic type Z, then X is a subtype of the principal instantiation of Z for Y.

3.7.7. Realizations

Given a member declared by Y, and a declaration that refines it, we can construct a refined realization of the member or nested type:

  • first determine the principal instantiation of Y for the class or interface which refines the member, and then

  • substitute the type arguments in this principal instantiation into the member schema.

Given an unqualified reference, as defined in §5.1.7 Unqualified reference resolution, to a declaration, and, in the case of a generic declaration, a list of type arguments for the type parameters of the declaration, we can construct an unqualified realization of the declaration:

  • if the declaration is a member declared by a type Y, first determine the principal instantiation of Y for the inheriting or declaring class or interface, and then

  • again, only if the declaration is a member declared by a type, substitute the type arguments in this principal instantiation into the declaration schema, and, finally,

  • substitute the type arguments into the declaration schema.

Given a qualified reference, as defined in §5.1.8 Qualified reference resolution, with a qualifying type X, to a member or nested type declared by Y, and, in the case of a generic member or generic nested type, a list of type arguments for the type parameters of the member, we can construct a qualified realization of the member or nested type:

  • first determining the principal instantiation of Y for X, and then

  • substituting the type arguments in this principal instantiation into the declaration schema, and, finally,

  • in the case of a generic member or generic nested type, substituting the type arguments into the declaration schema.

If, for any given qualified or unqualified reference, it is impossible to form the principal instantiation of the type that declares the referenced declaration, due to the hole described above in §3.7.4 Principal instantiation of a supertype, it is impossible to form a realization, and the reference to the declaration is illegal.