# Relay\'s Type System

We briefly introduced types while detailing Relay's expression language, but have not yet described its type system. Relay is a statically typed and type-inferred language, allowing programs to be fully typed while requiring just a few explicit type annotations.

Static types are useful when performing compiler optimizations because they communicate properties about the data a program manipulates, such as runtime shape, data layout, and storage, without needing to run the program. Relay's Algebraic Data Types allow for easily and flexibly composing types in order to build data structures that can be reasoned about inductively and used to write recursive functions.

Relay's type system features a form of *dependent typing* for shapes.
That is, its type system keeps track of the shapes of tensors in a Relay
program. Treating tensor shapes as types allows Relay to perform more
powerful reasoning at compile time; in particular, Relay can statically
reason about operations whose output shapes vary based on the input
shapes in complex ways. Casting shape inference as a type inference
problem allows Relay to infer the shapes of all tensors at compile time,
including in programs that use branching and function calls.

Statically reasoning about shapes in this manner allows Relay to be
ahead-of-time compiled and provides much more information about tensors
for optimizations further in the compilation pipeline. Such
optimizations can be implemented as passes, which are Relay-to-Relay AST
transformations, and may use the inferred types (e.g., shape
information) for making decisions about program transformations. For
instance, `src/relay/transforms/fuse_ops.cc`

gives an implementation of
a pass that uses inferred tensor shapes to replace invocations of
operators in a Relay program with fused operator implementations.

Reasoning about tensor types in Relay is encoded using *type relations*,
which means that the bulk of type checking in Relay is constraint
solving (ensuring that all type relations are satisfied at call sites).
Type relations offer a flexible and relatively simple way of making the
power of dependent typing available in Relay without greatly increasing
the complexity of its type system.

Below we detail the language of types in Relay and how they are assigned to Relay expressions.

## Type

The base type for all Relay types. All Relay types are sub-classes of this base type.

See `Type`

for its
definition and documentation.

## Tensor Type

A concrete tensor type in Relay.

Tensors are typed according to data type and shape. At present, these
use TVM's data types and shapes, but in the future, Relay may include a
separate AST for shapes. In particular, data types include `bool`

,
`float32`

, `int8`

and various other bit widths and numbers of lanes.
Shapes are given as tuples of dimensions (TVM `IndexExpr`

), such as
`(5, 5)`

; scalars are also given tuple types and have a shape of `()`

.

Note, though, that TVM shapes can also include variables and arithmetic expressions including variables, so Relay's constraint solving phase will attempt to find assignments to all shape variables to ensure all shapes will be concrete before running a program.

For example, here is a simple concrete tensor type corresponding to a 10-by-10 tensor of 32-bit floats:

`Tensor[(10, 10), float32]`

See `TensorType`

for
its definition and documentation.

## Tuple Type

A type of a tuple in Relay.

Just as a tuple is simply a sequence of values of statically known length, the type of a tuple consists of a sequence of the types corresponding to each member of the tuple.

Because a tuple type is of statically known size, the type of a tuple projection is simply the corresponding index into the tuple type.

For example, in the below code, `%t`

is of type
`(Tensor[(), bool], Tensor[(10, 10), float32])`

and `%c`

is of type
`Tensor[(10, 10), float32]`

.

`let %t = (False, Constant(1, (10, 10), float32));`

let %c = %t.1;

%c

See `TupleType`

for its
definition and documentation.

## Type Parameter

Type parameters represent placeholder types used for polymorphism in
functions. Type parameters are specified according to *kind*,
corresponding to the types those parameters are allowed to replace:

`Type`

, corresponding to top-level Relay types like tensor types, tuple types, and function types`BaseType`

, corresponding to the base type of a tensor (e.g.,`float32`

,`bool`

)`Shape`

, corresponding to a tensor shape`ShapeVar`

, corresponding to variables within a tensor shape

Relay's type system enforces that type parameters are only allowed to
appear where their kind permits them, so if type variable `t`

is of kind
`Type`

, `Tensor[t, float32]`

is not a valid type.

Like normal parameters, concrete arguments must be given for type parameters at call sites.

For example, `s`

below is a type parameter of kind `Shape`

and it will
be substituted with `(10, 10)`

at the call site below:

`def @plus<s : Shape>(%t1 : Tensor[s, float32], %t2 : Tensor[s, float32]) {`

add(%t1, %t2)

}

plus<(10, 10)>(%a, %b)

See `TypeVar`

for its
definition and documentation.

## Type Constraint

This is an abstract class representing a type constraint, to be elaborated upon in further releases. Currently, type relations are the only type constraints provided; they are discussed below.

See `TypeConstraint`

for its definition and documentation.

## Function Type

A function type in Relay, see [tvm/relay/type.h] for more details.

This is the type assigned to functions in Relay. A function type consists of a list of type parameters, a set of type constraints, a sequence of argument types, and a return type.

We informally write function types as:
`fn<type_params>(arg_types) -> ret_type where type_constraints`

A type parameter in the function type may appear in the argument types or the return types. Additionally, each of the type constraints must hold at every call site of the function. The type constraints typically take the function's argument types and the function's return type as arguments, but may take a subset instead.

See `FuncType`

for its
definition and documentation.

## Type Relation

A type relation is the most complex type system feature in Relay. It
allows users to extend type inference with new rules. We use type
relations to define types for operators that work with tensor shapes in
complex ways, such as broadcasting operators or `flatten`

, allowing
Relay to statically reason about the shapes in these cases.

A type relation `R`

describes a relationship between the input and
output types of a Relay function. Namely, `R`

is a function on types
that outputs [true] if the relationship holds and
[false] if it fails to hold. Types given to a relation may
be incomplete or include shape variables, so type inference must assign
appropriate values to incomplete types and shape variables for necessary
relations to hold, if such values exist.

For example we can define an identity relation to be:

`Identity(I, I) :- true`

It is usually convenient to type operators in Relay by defining a
relation specific to that operator that encodes all the necessary
constraints on the argument types and the return type. For example, we
can define the relation for `flatten`

:

`Flatten(Tensor(sh, bt), O) :-`

O = Tensor(sh[0], prod(sh[1:]))

If we have a relation like `Broadcast`

it becomes possible to type
operators like `add`

:

`add : fn<t1 : Type, t2 : Type, t3 : Type>(t1, t2) -> t3`

where Broadcast

The inclusion of `Broadcast`

above indicates that the argument types and
the return type must be tensors where the shape of `t3`

is the broadcast
of the shapes of `t1`

and `t2`

. The type system will accept any argument
types and return type so long as they fulfill `Broadcast`

.

Note that the above example relations are written in Prolog-like syntax,
but currently the relations must be implemented by users in C++ or
Python. More specifically, Relay's type system uses an *ad hoc* solver
for type relations in which type relations are actually implemented as
C++ or Python functions that check whether the relation holds and
imperatively update any shape variables or incomplete types. In the
current implementation, the functions implementing relations should
return `False`

if the relation fails to hold and `True`

if the relation
holds or if there is not enough information to determine whether it
holds or not.

The functions for all the relations are run as needed (if an input is updated) until one of the following conditions holds:

- All relations hold and no incomplete types remain (typechecking succeeds).
- A relation fails to hold (a type error).
- A fixpoint is reached where shape variables or incomplete types remain (either a type error or more type annotations may be needed).

Presently all of the relations used in Relay are implemented in C++. See
the files in `src/relay/op`

for examples of relations implemented in
C++.

See `TypeRelation`

for
its definition and documentation.

## Incomplete Type

An incomplete type is a type or portion of a type that is not yet known. This is only used during type inference. Any omitted type annotation is replaced by an incomplete type, which will be replaced by another type at a later point.

Incomplete types are known as "type variables" or "type holes" in the programming languages literature. We use the name "incomplete type" in order to more clearly distinguish them from type parameters: Type parameters must be bound to a function and are replaced with concrete type arguments (instantiated) at call sites, whereas incomplete types may appear anywhere in the program and are filled in during type inference.

See `IncompleteType`

for its definition and documentation.

## Algebraic Data Types

*Note: ADTs are not currently supported in the text format.*

Algebraic data types (ADTs) are described in more detail in
`their overview <adt-overview>`

; this
section describes their implementation in the type system.

An ADT is defined by a collection of named constructors, each of which takes arguments of certain types. An instance of an ADT is a container that stores the values of the constructor arguments used to produce it as well as the name of the constructor; the values can be retrieved by deconstructing the instance by matching based on its constructor. Hence, ADTs are sometimes called "tagged unions": like a C-style union, the contents of an instance for a given ADT may have different types in certain cases, but the constructor serves as a tag to indicate how to interpret the contents.

From the type system's perspective, it is most pertinent that ADTs can take type parameters (constructor arguments can be type parameters, though ADT instances with different type parameters must be treated as different types) and be recursive (a constructor for an ADT can take an instance of that ADT, thus an ADT like a tree or list can be inductively built up). The representation of ADTs in the type system must be able to accommodate these facts, as the below sections will detail.

### Global Type Variable

To represent ADTs compactly and easily allow for recursive ADT definitions, an ADT definition is given a handle in the form of a global type variable that uniquely identifies it. Each ADT definition is given a fresh global type variable as a handle, so pointer equality can be used to distinguish different ADT names.

For the purposes of Relay's type system, ADTs are differentiated by name; that means that if two ADTs have different handles, they will be considered different types even if all their constructors are structurally identical.

Recursion in an ADT definition thus follows just like recursion for a global function: the constructor can simply reference the ADT handle (global type variable) in its definition.

See `GlobalTypeVar`

for
its definition and documentation.

### Definitions (Type Data)

Besides a name, an ADT needs to store the constructors that are used to
define it and any type parameters used within them. These are stored in
the module,
`analogous to global function definitions<module-description>`

.

While type-checking uses of ADTs, the type system sometimes must index into the module using the ADT name to look up information about constructors. For example, if a constructor is being pattern-matched in a match expression clause, the type-checker must check the constructor's signature to ensure that any bound variables are being assigned the correct types.

See `TypeData`

for its
definition and documentation.

### Type Call

Because an ADT definition can take type parameters, Relay's type system
considers an ADT definition to be a *type-level function* (in that the
definition takes type parameters and returns the type of an ADT instance
with those type parameters). Thus, any instance of an ADT is typed using
a type call, which explicitly lists the type parameters given to the ADT
definition.

It is important to list the type parameters for an ADT instance, as two
ADT instances built using different constructors but the same type
parameters are of the *same type* while two ADT instances with different
type parameters should not be considered the same type (e.g., a list of
integers should not have the same type as a list of pairs of floating
point tensors).

The "function" in the type call is the ADT handle and there must be one argument for each type parameter in the ADT definition. (An ADT definition with no arguments means that any instance will have no type arguments passed to the type call).

See `TypeCall`

for its
definition and documentation.

### Example: List ADT

This subsection uses the simple list ADT (included as a default ADT in Relay) to illustrate the constructs described in the previous sections. Its definition is as follows:

`data List<a> {`

Nil : () -> List

Cons : (a, List[a]) -> List

}

Thus, the global type variable `List`

is the handle for the ADT. The
type data for the list ADT in the module notes that `List`

takes one
type parameter and has two constructors, `Nil`

(with signature
`fn<a>() -> List[a]`

) and `Cons`

(with signature
`fn<a>(a, List[a]) -> List[a]`

). The recursive reference to `List`

in
the `Cons`

constructor is accomplished by using the global type variable
`List`

in the constructor definition.

Below two instances of lists with their types given, using type calls:

`Cons(1, Cons(2, Nil())) # List[Tensor[(), int32]]`

Cons((1, 1), Cons((2, 2), Nil())) # List[(Tensor[(), int32], Tensor[(), int32])]

Note that `Nil()`

can be an instance of any list because it does not
take any arguments that use a type parameter. (Nevertheless, for any
*particular* instance of `Nil()`

, the type parameter must be specified.)

Here are two lists that are rejected by the type system because the type parameters do not match:

`# attempting to put an integer on a list of int * int tuples`

Cons(1, Cons((1, 1), Nil()))

# attempting to put a list of ints on a list of lists of int * int tuples

Cons(Cons(1, Cons(2, Nil())), Cons(Cons((1, 1), Cons((2, 2), Nil())), Nil()))