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:

*subtype polymorphism*, where a subtype`B`inherits a supertype`A`, and*parametric polymorphism*, where a type definition`A<T>`is parameterized by a*generic type parameter*`T`.

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:

An

*interface*, defined in §4.4 Interfaces, is an abstract type schema that cannot itself be directly instantiated. An interface may define concrete members, but these members may not hold references to other objects. A class may inherit one or more interfaces. An instance of a class that inherits an interface is also considered an instance of the interface.A

*generic type parameter*, defined in §3.5 Generic type parameters, is considered a type within the declaration that it parameterizes. In fact, it is an abstraction over many types: it generalizes the declaration to all types which could be assigned to the parameter.An

*applied type*, defined in §3.6 Generic type arguments, is formed by specifying arguments for the generic type parameters of a parameterized type declaration, and is called an*instantiation*of the parameterized type declaration.A

*union type*, defined in §3.2.3 Union types, is a type to which each of an enumerated list of types is assignable.An

*intersection type*, defined in §3.2.4 Intersection types, is a type which is assignable to each of an enumerated list of types.

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.

A

*type alias*, defined in §4.6 Type aliases, §4.5.9 Class aliases, and §4.4.5 Interface aliases, is a synonym for an expression involving other types or generic types. A type alias may itself be generic.

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:

What is the type of a variable that may or may not hold a value of type

`Element`?What is the type of a parameter that accepts either an

`Integer`or a`Float`?What is the type of a parameter that accepts values which are instances of both

`Persistent`and`Printable`?What is the type of a function which accepts any non-null value and returns a

`String`?What is the type of a function that accepts one or more

`String`s and returns an iterable object producing at least one`String`?What is the type of a sequence consisting of a

`String`followed by two`Float`s?What is the type of a list with no elements?

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.

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.

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.

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.

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`.

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`.

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`.

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`.

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.

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>

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`*`, anda

*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).

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:

be annotated

`shared`, as defined in §5.1.3 Visibility,occur as a toplevel declaration in a compilation unit, as defined in §4.1.1 Toplevel and nested declarations, or

be referred to by statements or declarations that occur earlier in the body containing of the declaration, as defined in §5.1 Block structure and references.

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.

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.

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

a class may

*extend*another class, as defined by §4.5.4 Class inheritance,a class may

*satisfy*one or more interfaces, as defined by §4.5.4 Class inheritance,an interface may

*satisfy*one or more other interfaces, as defined by §4.4.2 Interface inheritance, ora type parameter may

*satisfy*a class and/or one or more interfaces or type parameters, as defined by §3.5.3 Generic type constraints.

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.

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`.

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.

If the qualifier

`super`occurs, the specification is treated as a member expression, as defined by §6.5.2 Member expressions, where the qualifier`super`is treated according to §6.3.3 super.If a qualifying type occurs, the specification is treated as a constructor expression, as defined by §6.5.3 Constructor expressions.

Otherwise, if no qualifier occurs, the specification is treated as a base expression, as defined by §6.5.1 Base expressions.

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.

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.

*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.

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!

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, ora 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.

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).

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`.

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.

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>

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.

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 of`switch`
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.

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.

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.

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`.

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, ora 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, oras 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.

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, orboth

`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>`.

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`, andthe 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`, andthe 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 `Ai`s for their
corresponding `Pi`s 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.

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.

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.

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`.

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`, orfor 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`, orotherwise,

`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`, orif 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.

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`, orif 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`, orif 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.

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.

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`.

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 thensubstitute 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 thenagain, 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 thensubstituting 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.