Stanza's Type SystemTypes 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 TypesThere are only a handful of basic kinds of types in Stanza. Here is a listing of them all.
 Ground Types (e.g.
Int , String , True )
 Parametric Types (e.g.
Array<Int> , List<String> )
 Tuple Types (e.g.
[Int] , [Int, String] , [Int, True, String] )
 Function Types (e.g.
Int > String , (Int, Int) > Int )
 Union Types (e.g.
IntString , TrueFalse , CircleRectanglePoint )
 Intersection Types (e.g.
Collection<Int>&Lengthable )
 Void Type (
Void )
 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 RelationStanza'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 TypesGround 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 TypesParametric 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 TypesTuple 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 twoelement 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<T1T2...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<T1T2...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<IntIntInt> <: Collection<Int> because IntIntInt <: Int Function TypesFunction 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 TypesUnion types are used to represent a value who could either be of one type or another. The type IntString , 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, AB , if it can be proven that X is either a subtype of A or a subtype of B . X <: AB if X <: A or X <: B
For example, we can derive Int <: IntString
from Int <: IntString 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, AB , 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 . AB <: X if A <: X and B <: X
For example, we can derive CircleRectanglePoint <: Shape
from Circle  (RectanglePoint) <: Shape because Circle <: Shape and RectanglePoint <: Shape because Rectangle <: Shape and Point <: Shape
This rule is what causes Stanza to error if you attempt to pass a IntString object to a function that requires an Int object. Intersection TypesIntersection 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 TypeThe 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 TypeThe 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 dynamicallytyped 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.
