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 Shape
deftype 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 <: Int
String <: String
True <: 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 <: P
T <: X if P <: X

Thus we can derive

Circle <: Shape

from

Assuming deftype Circle <: Shape
Circle <: 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> <: P
A<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> <: P
A<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.