# Stanza's Type System

Types are the basis for how Stanza decides whether expressions are legal or not, and how to select the appropriate version of an overloaded function. This chapter will explain the different kinds of types in Stanza, what values each type represents, and the subtype relation.

## Kinds of Types

There are only a handful of basic kinds of types in Stanza. Here is a listing of them all.

1. Ground Types (e.g. `Int`, `String`, `True`)
2. Parametric Types (e.g. `Array<Int>`, `List<String>`)
3. Tuple Types (e.g. `[Int]`, `[Int, String]`, `[Int, True, String]`)
4. Function Types (e.g. `Int -> String`, `(Int, Int) -> Int`)
5. Union Types (e.g. `Int|String`, `True|False`, `Circle|Rectangle|Point`)
6. Intersection Types (e.g. `Collection<Int>&Lengthable`)
7. Void Type (`Void`)
8. Unknown Type (`?`)

Each kind of type will be described in detail in this chapter. The only type that has not been introduced yet is the void type. Most importantly, we'll cover the subtyping rules for each kind of type, which are the rules that Stanza uses to determine whether a program is legal.

## The Subtype Relation

Stanza's type system is built upon the subtyping relation. The most important operation on types is determining whether one type is a subtype of another.  We use the following notation

``A <: B``

to indicate that the type `A` is a subtype of the type `B`. Intuitively, what this means is that Stanza will allow you to pass a value of type `A` to any place that is expecting a value of type `B`.

In previous chapters, we have demonstrated examples using the types

``deftype Shapedeftype Circle <: Shape``

According to these definitions, the `Circle` type is a subtype of `Shape`.

``Circle <: Shape``

This means that we may pass a `Circle` to any place that is expecting a `Shape`. For example, we can call functions that accept `Shape` arguments with `Circle` objects. We can initialize values and variables of type `Shape` with `Circle` objects. And we can return `Circle` objects from functions annotated to return `Shape` objects.

Whether one type is a subtype of another is calculated from a set of subtyping rules. There is a small set for handling each kind of type, and we'll introduce them to you gradually.

## Ground Types

Ground types are the most basic types in Stanza and are simply types that don't take any type parameters. The majority of types used in daily programming are simple ground types. `Int`, `String`, `True`, `False`, and `Char` are a few examples of ground types that you've used.

### Reflexivity Rule

There are two subtyping rules for ground types. The first is that a ground type is a subtype of itself.

``T <: T``

This rule is almost trivial. For example, here are some relations derivable from this rule.

``Int <: IntString <: StringTrue <: True``

meaning that you can call a function that accepts `String` with an `String` object.

### Parent Rule

Users may define their own ground types using `deftype`. For example, here is the type declaration for `Circle` again.

``deftype Circle <: Shape``

The general form for `deftype` is

``deftype T <: P``

Here is the second subtyping rule for ground types. The type `T` is a subtype of `X` if it can be proven that its parent type `P` is a subtype of `X`.

``Assuming deftype T <: PT <: X if P <: X``

Thus we can derive

``Circle <: Shape``

from

``Assuming deftype Circle <: ShapeCircle <: Shape because Shape <: Shape``

This rule is what allows us to pass `Circle` objects to functions that accept `Shape` objects.

## Parametric Types

Parametric types are types that take one or more type parameters. `Array<Int>`, `List<String>`, and our own type, `Stack<String>`, are examples of parametric types.

### Covariance Rule

First consider the case where a base type, `A`, takes only a single type parameter. This rule says that a parametric type `A<T>` is a subtype of another parametric type `A<S>` if it can be proven that its type parameter, `T`, is a subtype of the other's type parameter, `S`.

``A<T> <: A<S> if T <: S``

In general, for arbitrary numbers of type parameters, the parametric type `A<T1,T2, ..., Tn>` is a subtype of another parametric type `A<S1, S2, ..., Sn>` if its type parameters, `T1`, `T2`, ..., `Tn` are respectively subtypes of the other's type parameters, `S1`, `S2`, ..., `Sn`.

``A<T1, T2, ..., Tn> <: A<S1, S2, ..., Sn> if   T1 <: S1 and   T2 <: S2 and   ...   Tn <: Sn``

For example, we can derive

``List<Circle> <: List<Shape>``

from

``List<Circle> <: List<Shape> because   Circle <: Shape``

This rule is what allows us to pass a list of circles to a function expecting a list of shapes.

### Parent Rule

Consider again the simple case where a base type, `A`, takes a single type parameter. Assume that `A` is defined the following way.

``deftype A<S> <: P``

The parent rule for parametric types says that the parametric type `A<T>` is a subtype of `X` if it can be proven that the result of replacing every occurrence of `S` in `P` with `T` is a subtype of `X`.

``Assuming deftype A<S> <: PA<T> <: X if P[S := T] <: X``

where the notation `P[S := T]` stands for the result of replacing every occurrence of `S` in `P` with `T`.

Our parametric `Stack` type, for example, is declared

``deftype Stack<T> <: Collection<T>``

We can derive

``Stack<Circle> <: Collection<Shape>``

from

``Stack<Circle> <: Collection<Shape> because   Collection<Circle> <: Collection<Shape> because      Circle <: Shape``

Here is the general form of the rule for arbitrary numbers of type parameters.

``Assuming deftype A<S1, S2, ..., Sn> <: PA<T1, T2, ..., Tn> <: X if   P[S1 := T1, S2 := T2, ..., Sn := Tn] <: X``

It says that the parametric type `A<T1, T2, ..., Tn>` is a subtype of `X` if it can be proven that the result of replacing every occurrence of `S1`, `S2`, ..., `Sn` in `P` respectively with `T1`, `T2`, ..., `Tn` is a subtype of `X`.

## Tuple Types

Tuple types are used for representing the types of tuple objects. They're special in that they take a variable number of type parameters. Here is an example of a tuple type. The type

``[Int, String]``

represents a two-element tuple, where the first element is an `Int` and the second element is a `String`.

### Covariance Rule

This rule says that the tuple type `[T1, T2, ..., Tn]` is a subtype of the tuple type `[S1, S2, ..., Sn]` if the types of the elements `T1`, `T2`, ..., `Tn` are respectively subtypes of the types of the other's elements `S1`, `S2`, ..., `Sn`.

``[T1, T2, ..., Tn] <: [S1, S2, ..., Sn] if   T1 <: S1 and   T2 <: S2 and   ...   Tn <: Sn``

For example, we can derive

``[Circle, Rectangle] <: [Shape, Shape]``

from

``[Circle, Rectangle] <: [Shape, Shape] because   Circle <: Shape and   Rectangle <: Shape``

### Collapsed Tuple Rule

The type `Tuple` is used to represent a tuple of unknown arity. This rule allows us to pass tuples with known arity to places expecting tuples with unknown arity.

``[T1, T2, ..., Tn] <: X if Tuple<T1|T2|...|Tn> <: X``

It says that a tuple of known arity containing elements of type `T1`, `T2`, ..., `Tn` is a subtype of `X` if it can be proven that the tuple of unknown arity `Tuple<T1|T2|...|Tn>` is a subtype of `X`.

The type `Tuple<T>` is defined to be a subtype of `Collection<T>` in the core library, so this rule is what allows us to pass in tuples to functions that expect collections. For example, we can derive

``[Int, Int, Int] <: Collection<Int>``

from

``[Int, Int, Int] <: Collection<Int> because   Tuple<Int|Int|Int> <: Collection<Int> because      Int|Int|Int <: Int``

## Function Types

Function types are used to represent the type of function objects. We've used them in the previous chapters to write functions that accept other functions as arguments.

Let us first consider just functions that take a single argument.

``T1 -> S1 <: T2 -> S2 if   S1 <: S2 and   T2 <: T1``

The rule says that a function type `T1 -> S1` is a subtype of another function type `T2 -> S2` if it can be proven that the return type of the first, `S1`, is a subtype of the return type of the second, `S2`, and if the argument type of the second, `T2`, is a subtype of the argument type of the first, `T1`.

### Covariance

This rule is a little confusing at first, so let's go it carefully. First, the following relation

``Int -> Circle <: Int -> Shape``

can be derived from

``Int -> Circle <: Int -> Shape because   Circle <: Shape and   Int <: Int``

Suppose we are calling a function, `f`, that requires a function argument. What this rule means is that if `f` requires its argument to return `Shape` objects, then we are allowed to pass it a function that returns `Circle` objects. This makes sense as all circles are shapes. So assuming that `f` calls its argument function, then whatever `f` will do with the resultant `Shape` objects, `f` can also do with `Circle` objects.

### Contravariance

Next, the following relation

``Shape -> Int <: Circle -> Int``

can be derived from

``Shape -> Int <: Circle -> Int because   Int <: Int and   Circle <: Shape``

Suppose we are again calling a function, `f`, that requires a function argument. What this rule means is that if `f` requires its argument to accept `Circle` objects, then we are allowed to pass it a function that accepts `Shape` objects. This makes sense as all functions that can accept `Shape` objects, can also accept `Circle` objects.

The general rule for function types results from the combination of functions being covariant in its return type and `contravariant` in its argument types.

### General Form

Here is the general form of the function subtyping rule for arbitrary numbers of arguments.

``(T1, T2, ..., Tn) -> R1 <: (S1, S2, ..., Sn) -> R2 if   R1 <: R2 and   S1 <: T1 and   S2 <: T2 and   ...   Sn <: Tn``

Thus a function type `(T1, T2, ..., Tn) -> R1` is a subtype of another function type `(S1, S2, ..., Sn) -> R2` if it can be proven that the return type of the first, `R1`, is a subtype of the return type of the second, `R2`, and the argument types of the second, `S1`, `S2`, ..., `Sn`, are respectively subtypes of the argument types of the first, `T1`, `T2`, ..., `Tn`.

## Union Types

Union types are used to represent a value who could either be of one type or another. The type `Int|String`, for example, represents a value that could either be an `Int` or a `String`.

### Expecting a Union Type

The following rule says that a type, `X`, is a subtype of a union type, `A|B`, if it can be proven that `X` is either a subtype of `A` or a subtype of `B`.

``X <: A|B if X <: A or X <: B``

For example, we can derive

``Int <: Int|String``

from

``Int <: Int|String because Int <: Int``

This rule allows us to write functions that accept a variety of types, and be allowed to pass it a specific one.

### Passing a Union Type

The following rule says that a union type, `A|B`, is a subtype of `X`, if it can be proven that both `A` is a subtype of `X` and `B` is a subtype of `X`.

``A|B <: X if A <: X and B <: X``

For example, we can derive

``Circle|Rectangle|Point <: Shape``

from

``Circle | (Rectangle|Point) <: Shape because   Circle <: Shape and   Rectangle|Point <: Shape because      Rectangle <: Shape and      Point <: Shape``

This rule is what causes Stanza to error if you attempt to pass a `Int|String` object to a function that requires an `Int` object.

## Intersection Types

Intersection types are the dual of union types, and are used to indicate that a value is both of one type and also of another. The type `Collection<Int> & Lengthable`, for example, represents an object that is simultaneously both a collection of integers and also a `Lengthable` object.

### Expecting an Intersection Type

The following rule says that a type, `X`, is a subtype of an intersection type, `A&B`, if it can be proven that `X` is both a subtype of `A` and also a subtype of `B`.

``X <: A&B if X <: A and X <: B``

For example, we can derive

``Stack<Int> <: Collection<Int> & Lengthable``

from

``Stack<Int> <: Collection<Int> & Lengthable because   Stack<Int> <: Collection<Int> and   Stack<Int> <: Lengthable``

### Passing an Intersection Type

The following rule says that an intersection type `A&B` is a subtype of `X` if it can be proven that either `A` is a subtype of `X` or `B` is a subtype of `X`.

``A&B <: X if A <: X or B <: X``

For example, we can derive

``Stack<Int> <: Lengthable``

from

``Stack<Int> <: Lengthable because   Collection<Int> & Lengthable <: Lengthable because      Lengthable <: Lengthable``

## The Void Type

The void type is a special type in Stanza that represents no value.

It is used, for example, as the return type of the `fatal` function, which simply prints an error message and then immediately quits the program. `fatal` never returns, so it's inappropriate to say that it returns any type. `throw` is another function that returns `Void`, as it also never returns to its caller.

It is occasionally also used as a type parameter for collection types. For example, the following call

``val xs = List()``

creates an object of type `List<Void>` and assigns it to `xs`. Recall that calling `head` on a value of type `List<T>` returns `T`. Similarly, calling `head` on a value of type `List<Void>` returns `Void`, indicating that such a call would not return.

The only subtyping rule for `Void` is that it is a subtype of any type, `T`.

``Void <: T``

For programmers familiar with the `void` type in the C and Java programming language, note that this is not the same concept. A C function that returns `void` still returns. It simply returns a meaningless value, so you're forbidden from using it for anything. In contrast, a Stanza function that returns `Void` does not return.

## The Unknown Type

The unknown type is a very important type and forms the basis of Stanza's optional typing system. There are two subtyping rules that defines its behaviour.

### Expecting an Unknown Type

The following rule says that any type, `T`, is a subtype of `?`.

``T <: ?``

When we declare a function that accepts arguments of type `?`, it is this rule that allows us to pass any object to the function.

### Passing an Unknown Type

The following rule says that the unknown type, `?`, is a subtype of any type, `T`.

``? <: T``

Given a value or argument declared with the `?` type, it is this rule that allows us to pass this value anywhere, regardless of what type is actually expected.

These two rules together allows Stanza to model the behaviour of dynamically-typed scripting languages in a principled manner. The behaviour of the Python programming language, for example, can be mimicked by declaring every argument and value as having the unknown type.