-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathchapter10.html
39 lines (38 loc) · 22.2 KB
/
chapter10.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
<!DOCTYPE html>
<html>
<head>
<title>L.B.Stanza</title>
<link type="text/css" rel="stylesheet" href="resources/mainstyle.css">
<link type="text/css" rel="stylesheet" href="resources/documentation.css">
</head>
<body>
<table class="wrap">
<tr><td colspan="3" class="banner">
<a href="index.html">Home</a><a href="stanzabyexample.html">Table of Contents</a><a href="macrosystem.html">Previous Chapter</a><a href="chapter11.html">Next Chapter</a>
</td></tr>
<tr>
<td class="nav">
<h1>NAVIGATION</h1>
<h2><a href="#anchor370">Stanza's Type System</a></h2><h3><a href="#anchor95">Kinds of Types</a></h3><h3><a href="#anchor96">The Subtype Relation</a></h3><h3><a href="#anchor97">Ground Types</a></h3><h4><a href="#anchor371">Reflexivity Rule</a></h4><h4><a href="#anchor372">Parent Rule</a></h4><h3><a href="#anchor98">Parametric Types</a></h3><h4><a href="#anchor373">Covariance Rule</a></h4><h4><a href="#anchor374">Parent Rule</a></h4><h3><a href="#anchor99">Tuple Types</a></h3><h4><a href="#anchor375">Covariance Rule</a></h4><h4><a href="#anchor376">Collapsed Tuple Rule</a></h4><h3><a href="#anchor100">Function Types</a></h3><h4><a href="#anchor377">Covariance</a></h4><h4><a href="#anchor378">Contravariance</a></h4><h4><a href="#anchor379">General Form</a></h4><h3><a href="#anchor101">Union Types</a></h3><h4><a href="#anchor380">Expecting a Union Type</a></h4><h4><a href="#anchor381">Passing a Union Type</a></h4><h3><a href="#anchor102">Intersection Types</a></h3><h4><a href="#anchor382">Expecting an Intersection Type</a></h4><h4><a href="#anchor383">Passing an Intersection Type</a></h4><h3><a href="#anchor103">The Void Type</a></h3><h3><a href="#anchor104">The Unknown Type</a></h3><h4><a href="#anchor384">Expecting an Unknown Type</a></h4><h4><a href="#anchor385">Passing an Unknown Type</a></h4>
</td>
<td class="main">
<h1 id="anchor370">Stanza's Type System</h1><p>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.</p><h2 id="anchor95">Kinds of Types</h2><p>There are only a handful of basic kinds of types in Stanza. Here is a listing of them all.</p><ol><li>Ground Types (e.g. <code>Int</code>, <code>String</code>, <code>True</code>)
</li><li>Parametric Types (e.g. <code>Array<Int></code>, <code>List<String></code>)
</li><li>Tuple Types (e.g. <code>[Int]</code>, <code>[Int, String]</code>, <code>[Int, True, String]</code>)
</li><li>Function Types (e.g. <code>Int -> String</code>, <code>(Int, Int) -> Int</code>)
</li><li>Union Types (e.g. <code>Int|String</code>, <code>True|False</code>, <code>Circle|Rectangle|Point</code>)
</li><li>Intersection Types (e.g. <code>Collection<Int>&Lengthable</code>)
</li><li>Void Type (<code>Void</code>)
</li><li>Unknown Type (<code>?</code>)
</li></ol><p>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 <span style="font-style:italic;">subtyping</span> rules for each kind of type, which are the rules that Stanza uses to determine whether a program is legal.</p><h2 id="anchor96">The Subtype Relation</h2><p>Stanza's type system is built upon the <span style="font-style:italic;">subtyping</span> relation. The most important operation on types is determining whether one type is a <span style="font-style:italic;">subtype</span> of another. We use the following notation</p><pre><code>A <: B</code></pre><p>to indicate that the type <code>A</code> is a subtype of the type <code>B</code>. Intuitively, what this means is that Stanza will allow you to pass a value of type <code>A</code> to any place that is expecting a value of type <code>B</code>.</p><p>In previous chapters, we have demonstrated examples using the types</p><pre><code>deftype Shape<br>deftype Circle <: Shape</code></pre><p>According to these definitions, the <code>Circle</code> type is a subtype of <code>Shape</code>.</p><pre><code>Circle <: Shape</code></pre><p>This means that we may pass a <code>Circle</code> to any place that is expecting a <code>Shape</code>. For example, we can call functions that accept <code>Shape</code> arguments with <code>Circle</code> objects. We can initialize values and variables of type <code>Shape</code> with <code>Circle</code> objects. And we can return <code>Circle</code> objects from functions annotated to return <code>Shape</code> objects.</p><p>Whether one type is a subtype of another is calculated from a set of <span style="font-style:italic;">subtyping rules</span>. There is a small set for handling each kind of type, and we'll introduce them to you gradually.</p><h2 id="anchor97">Ground Types</h2><p>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. <code>Int</code>, <code>String</code>, <code>True</code>, <code>False</code>, and <code>Char</code> are a few examples of ground types that you've used.</p><h3 id="anchor371">Reflexivity Rule</h3><p>There are two subtyping rules for ground types. The first is that a ground type is a subtype of itself.</p><pre><code>T <: T</code></pre><p>This rule is almost trivial. For example, here are some relations derivable from this rule.</p><pre><code>Int <: Int<br>String <: String<br>True <: True</code></pre><p>meaning that you can call a function that accepts <code>String</code> with an <code>String</code> object.</p><h3 id="anchor372">Parent Rule</h3><p>Users may define their own ground types using <code>deftype</code>. For example, here is the type declaration for <code>Circle</code> again.</p><pre><code>deftype Circle <: Shape</code></pre><p>The general form for <code>deftype</code> is</p><pre><code>deftype T <: P</code></pre><p>Here is the second subtyping rule for ground types. The type <code>T</code> is a subtype of <code>X</code> if it can be proven that its parent type <code>P</code> is a subtype of <code>X</code>.</p><pre><code>Assuming deftype T <: P<br>T <: X if P <: X</code></pre><p>Thus we can derive</p><pre><code>Circle <: Shape</code></pre><p>from</p><pre><code>Assuming deftype Circle <: Shape<br>Circle <: Shape because Shape <: Shape</code></pre><p>This rule is what allows us to pass <code>Circle</code> objects to functions that accept <code>Shape</code> objects.</p><h2 id="anchor98">Parametric Types</h2><p>Parametric types are types that take one or more <span style="font-style:italic;">type parameters</span>. <code>Array<Int></code>, <code>List<String></code>, and our own type, <code>Stack<String></code>, are examples of parametric types.</p><h3 id="anchor373">Covariance Rule</h3><p>First consider the case where a base type, <code>A</code>, takes only a single type parameter. This rule says that a parametric type <code>A<T></code> is a subtype of another parametric type <code>A<S></code> if it can be proven that its type parameter, <code>T</code>, is a subtype of the other's type parameter, <code>S</code>.</p><pre><code>A<T> <: A<S> if T <: S</code></pre><p>In general, for arbitrary numbers of type parameters, the parametric type <code>A<T1,T2, ..., Tn></code> is a subtype of another parametric type <code>A<S1, S2, ..., Sn></code> if its type parameters, <code>T1</code>, <code>T2</code>, ..., <code>Tn</code> are respectively subtypes of the other's type parameters, <code>S1</code>, <code>S2</code>, ..., <code>Sn</code>.</p><pre><code>A<T1, T2, ..., Tn> <: A<S1, S2, ..., Sn> if<br> T1 <: S1 and<br> T2 <: S2 and<br> ...<br> Tn <: Sn</code></pre><p>For example, we can derive</p><pre><code>List<Circle> <: List<Shape></code></pre><p>from</p><pre><code>List<Circle> <: List<Shape> because<br> Circle <: Shape</code></pre><p>This rule is what allows us to pass a list of circles to a function expecting a list of shapes.</p><h3 id="anchor374">Parent Rule</h3><p>Consider again the simple case where a base type, <code>A</code>, takes a single type parameter. Assume that <code>A</code> is defined the following way.</p><pre><code>deftype A<S> <: P</code></pre><p>The parent rule for parametric types says that the parametric type <code>A<T></code> is a subtype of <code>X</code> if it can be proven that the result of replacing every occurrence of <code>S</code> in <code>P</code> with <code>T</code> is a subtype of <code>X</code>.</p><pre><code>Assuming deftype A<S> <: P<br>A<T> <: X if P[S := T] <: X</code></pre><p>where the notation <code>P[S := T]</code> stands for the result of replacing every occurrence of <code>S</code> in <code>P</code> with <code>T</code>.</p><p>Our parametric <code>Stack</code> type, for example, is declared</p><pre><code>deftype Stack<T> <: Collection<T></code></pre><p>We can derive</p><pre><code>Stack<Circle> <: Collection<Shape></code></pre><p>from</p><pre><code>Stack<Circle> <: Collection<Shape> because<br> Collection<Circle> <: Collection<Shape> because<br> Circle <: Shape</code></pre><p>Here is the general form of the rule for arbitrary numbers of type parameters.</p><pre><code>Assuming deftype A<S1, S2, ..., Sn> <: P<br>A<T1, T2, ..., Tn> <: X if<br> P[S1 := T1, S2 := T2, ..., Sn := Tn] <: X</code></pre><p>It says that the parametric type <code>A<T1, T2, ..., Tn></code> is a subtype of <code>X</code> if it can be proven that the result of replacing every occurrence of <code>S1</code>, <code>S2</code>, ..., <code>Sn</code> in <code>P</code> respectively with <code>T1</code>, <code>T2</code>, ..., <code>Tn</code> is a subtype of <code>X</code>.</p><h2 id="anchor99">Tuple Types</h2><p>Tuple types are used for representing the types of tuple objects. They're special in that they take a <span style="font-style:italic;">variable</span> number of type parameters. Here is an example of a tuple type. The type</p><pre><code>[Int, String]</code></pre><p>represents a two-element tuple, where the first element is an <code>Int</code> and the second element is a <code>String</code>.</p><h3 id="anchor375">Covariance Rule</h3><p>This rule says that the tuple type <code>[T1, T2, ..., Tn]</code> is a subtype of the tuple type <code>[S1, S2, ..., Sn]</code> if the types of the elements <code>T1</code>, <code>T2</code>, ..., <code>Tn</code> are respectively subtypes of the types of the other's elements <code>S1</code>, <code>S2</code>, ..., <code>Sn</code>.</p><pre><code>[T1, T2, ..., Tn] <: [S1, S2, ..., Sn] if<br> T1 <: S1 and<br> T2 <: S2 and<br> ...<br> Tn <: Sn</code></pre><p>For example, we can derive</p><pre><code>[Circle, Rectangle] <: [Shape, Shape]</code></pre><p>from</p><pre><code>[Circle, Rectangle] <: [Shape, Shape] because<br> Circle <: Shape and<br> Rectangle <: Shape</code></pre><h3 id="anchor376">Collapsed Tuple Rule</h3><p>The type <code>Tuple</code> is used to represent a tuple of <span style="font-style:italic;">unknown</span> arity. This rule allows us to pass tuples with known arity to places expecting tuples with unknown arity.</p><pre><code>[T1, T2, ..., Tn] <: X if Tuple<T1|T2|...|Tn> <: X</code></pre><p>It says that a tuple of known arity containing elements of type <code>T1</code>, <code>T2</code>, ..., <code>Tn</code> is a subtype of <code>X</code> if it can be proven that the tuple of unknown arity <code>Tuple<T1|T2|...|Tn></code> is a subtype of <code>X</code>.</p><p>The type <code>Tuple<T></code> is defined to be a subtype of <code>Collection<T></code> 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</p><pre><code>[Int, Int, Int] <: Collection<Int></code></pre><p>from</p><pre><code>[Int, Int, Int] <: Collection<Int> because<br> Tuple<Int|Int|Int> <: Collection<Int> because<br> Int|Int|Int <: Int</code></pre><h2 id="anchor100">Function Types</h2><p>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.</p><p>Let us first consider just functions that take a single argument.</p><pre><code>T1 -> S1 <: T2 -> S2 if<br> S1 <: S2 and<br> T2 <: T1</code></pre><p>The rule says that a function type <code>T1 -> S1</code> is a subtype of another function type <code>T2 -> S2</code> if it can be proven that the return type of the first, <code>S1</code>, is a subtype of the return type of the second, <code>S2</code>, and if the argument type of the second, <code>T2</code>, is a subtype of the argument type of the first, <code>T1</code>.</p><h3 id="anchor377">Covariance</h3><p>This rule is a little confusing at first, so let's go it carefully. First, the following relation</p><pre><code>Int -> Circle <: Int -> Shape</code></pre><p>can be derived from</p><pre><code>Int -> Circle <: Int -> Shape because<br> Circle <: Shape and<br> Int <: Int</code></pre><p>Suppose we are calling a function, <code>f</code>, that requires a function argument. What this rule means is that if <code>f</code> requires its argument to return <code>Shape</code> objects, then we are allowed to pass it a function that returns <code>Circle</code> objects. This makes sense as all circles are shapes. So assuming that <code>f</code> calls its argument function, then whatever <code>f</code> will do with the resultant <code>Shape</code> objects, <code>f</code> can also do with <code>Circle</code> objects.</p><h3 id="anchor378">Contravariance</h3><p>Next, the following relation</p><pre><code>Shape -> Int <: Circle -> Int</code></pre><p>can be derived from</p><pre><code>Shape -> Int <: Circle -> Int because<br> Int <: Int and<br> Circle <: Shape</code></pre><p>Suppose we are again calling a function, <code>f</code>, that requires a function argument. What this rule means is that if <code>f</code> requires its argument to accept <code>Circle</code> objects, then we are allowed to pass it a function that accepts <code>Shape</code> objects. This makes sense as all functions that can accept <code>Shape</code> objects, can also accept <code>Circle</code> objects.</p><p>The general rule for function types results from the combination of functions being <span style="font-style:italic;">covariant</span> in its return type and <code>contravariant</code> in its argument types.</p><h3 id="anchor379">General Form</h3><p>Here is the general form of the function subtyping rule for arbitrary numbers of arguments.</p><pre><code>(T1, T2, ..., Tn) -> R1 <: (S1, S2, ..., Sn) -> R2 if<br> R1 <: R2 and<br> S1 <: T1 and<br> S2 <: T2 and<br> ...<br> Sn <: Tn</code></pre><p>Thus a function type <code>(T1, T2, ..., Tn) -> R1</code> is a subtype of another function type <code>(S1, S2, ..., Sn) -> R2</code> if it can be proven that the return type of the first, <code>R1</code>, is a subtype of the return type of the second, <code>R2</code>, and the argument types of the second, <code>S1</code>, <code>S2</code>, ..., <code>Sn</code>, are respectively subtypes of the argument types of the first, <code>T1</code>, <code>T2</code>, ..., <code>Tn</code>.</p><h2 id="anchor101">Union Types</h2><p>Union types are used to represent a value who could either be of one type or another. The type <code>Int|String</code>, for example, represents a value that could either be an <code>Int</code> or a <code>String</code>.</p><h3 id="anchor380">Expecting a Union Type</h3><p>The following rule says that a type, <code>X</code>, is a subtype of a union type, <code>A|B</code>, if it can be proven that <code>X</code> is either a subtype of <code>A</code> or a subtype of <code>B</code>.</p><pre><code>X <: A|B if X <: A or X <: B</code></pre><p>For example, we can derive</p><pre><code>Int <: Int|String</code></pre><p>from</p><pre><code>Int <: Int|String because Int <: Int</code></pre><p>This rule allows us to write functions that accept a variety of types, and be allowed to pass it a specific one.</p><h3 id="anchor381">Passing a Union Type</h3><p>The following rule says that a union type, <code>A|B</code>, is a subtype of <code>X</code>, if it can be proven that both <code>A</code> is a subtype of <code>X</code> and <code>B</code> is a subtype of <code>X</code>.</p><pre><code>A|B <: X if A <: X and B <: X</code></pre><p>For example, we can derive</p><pre><code>Circle|Rectangle|Point <: Shape</code></pre><p>from</p><pre><code>Circle | (Rectangle|Point) <: Shape because<br> Circle <: Shape and<br> Rectangle|Point <: Shape because<br> Rectangle <: Shape and<br> Point <: Shape</code></pre><p>This rule is what causes Stanza to error if you attempt to pass a <code>Int|String</code> object to a function that requires an <code>Int</code> object.</p><h2 id="anchor102">Intersection Types</h2><p>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 <code>Collection<Int> & Lengthable</code>, for example, represents an object that is simultaneously both a collection of integers and also a <code>Lengthable</code> object.</p><h3 id="anchor382">Expecting an Intersection Type</h3><p>The following rule says that a type, <code>X</code>, is a subtype of an intersection type, <code>A&B</code>, if it can be proven that <code>X</code> is both a subtype of <code>A</code> and also a subtype of <code>B</code>.</p><pre><code>X <: A&B if X <: A and X <: B</code></pre><p>For example, we can derive</p><pre><code>Stack<Int> <: Collection<Int> & Lengthable</code></pre><p>from</p><pre><code>Stack<Int> <: Collection<Int> & Lengthable because<br> Stack<Int> <: Collection<Int> and<br> Stack<Int> <: Lengthable</code></pre><h3 id="anchor383">Passing an Intersection Type</h3><p>The following rule says that an intersection type <code>A&B</code> is a subtype of <code>X</code> if it can be proven that either <code>A</code> is a subtype of <code>X</code> or <code>B</code> is a subtype of <code>X</code>.</p><pre><code>A&B <: X if A <: X or B <: X</code></pre><p>For example, we can derive</p><pre><code>Stack<Int> <: Lengthable</code></pre><p>from</p><pre><code>Stack<Int> <: Lengthable because<br> Collection<Int> & Lengthable <: Lengthable because<br> Lengthable <: Lengthable</code></pre><h2 id="anchor103">The Void Type</h2><p>The void type is a special type in Stanza that represents <span style="font-style:italic;">no value</span>.</p><p>It is used, for example, as the return type of the <code>fatal</code> function, which simply prints an error message and then immediately quits the program. <code>fatal</code> never returns, so it's inappropriate to say that it returns <span style="font-style:italic;">any</span> type. <code>throw</code> is another function that returns <code>Void</code>, as it also never returns to its caller.</p><p>It is occasionally also used as a type parameter for collection types. For example, the following call</p><pre><code>val xs = List()</code></pre><p>creates an object of type <code>List<Void></code> and assigns it to <code>xs</code>. Recall that calling <code>head</code> on a value of type <code>List<T></code> returns <code>T</code>. Similarly, calling <code>head</code> on a value of type <code>List<Void></code> returns <code>Void</code>, indicating that such a call would not return.</p><p>The only subtyping rule for <code>Void</code> is that it is a subtype of any type, <code>T</code>.</p><pre><code>Void <: T</code></pre><p>For programmers familiar with the <code>void</code> type in the C and Java programming language, note that this is not the same concept. A C function that returns <code>void</code> still returns. It simply returns a meaningless value, so you're forbidden from using it for anything. In contrast, a Stanza function that returns <code>Void</code> <span style="font-style:italic;">does not return</span>.</p><h2 id="anchor104">The Unknown Type</h2><p>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.</p> <h3 id="anchor384">Expecting an Unknown Type</h3><p> The following rule says that <span style="font-style:italic;">any</span> type, <code>T</code>, is a subtype of <code>?</code>.</p><pre><code>T <: ?</code></pre><p>When we declare a function that accepts arguments of type <code>?</code>, it is this rule that allows us to pass any object to the function.</p><h3 id="anchor385">Passing an Unknown Type</h3><p>The following rule says that the unknown type, <code>?</code>, is a subtype of <span style="font-style:italic;">any</span> type, <code>T</code>.</p><pre><code>? <: T</code></pre><p>Given a value or argument declared with the <code>?</code> type, it is this rule that allows us to pass this value anywhere, regardless of what type is actually expected.</p><p>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.</p>
</td>
<td class="rest">
<img url="resources/spacer.gif"></img>
</td>
</tr>
<tr><td colspan="3" class="footer">
Site design by Luca Li. Copyright 2015.
</td></tr>
</table>
</body>
</html>