Notes on Typed Racket for CMSC 15100

Racket is a dynamically typed language, which means that type errors are not detected until the erroneous code is actually executed. For example, we might define a function for squaring numbers.

If we then attempt to apply it to two arguments or to the wrong kind of argument, we get a runtime type error

In this simple example, waiting until runtime to find the error is not a big deal, but in larger programs such errors can be hidden from immediate detection. For example, consider the following (erroneous) function

Testing this function might not expose the error, since the error occurs on only one branch of the conditional. For example:

In this simple example, an additional test case is sufficient to detect the error, but, in general, it may involve a significant amount of testing to check all of the potential dynamic type errors.

In Typed Racket, we write the type signature (or contract) of a function as part of the program’s syntax, instead of just as a comment. Returning to out sq function, we would write it in Typed Racket as follows:

The first line is a directive that tells the Racket system that we are using the Typed Racket language. You will include this directive in all of your programs. The definition of the sq function is still three lines, but the first line is now a type annotation that tells the system what the type of the sq function is (a function from Number to Number).

Typed Racket divides numbers into many different types based on properties such as whether they are rational, integral, or not, their sign (positive or negitive), and how large their computer representation is. For this course, we use a small subset of these types, which are effectively organized in a heirarchy. We list them here in order of containment (_i.e., each type contains all of the previous types):

are all examples of symbols.

Functions in racket take zero or more arguments and return a single result. We write the type of a function by listing the argument types, followed by the → symbol and the result type. For example, the type of a function that takes an Integer argument and a Boolean argument and returns a string is written as follows:

As in the Chapter 6 of the textbook, Typed Racket provides the define-struct special form. The main difference is that unlike the form described in the book, in Typed Racket we must specify the types of the structure components. For example:

The other noticable difference is the #:transparent option, which tells Typed Racket to make this a transparent type (as opposed to an opaque type). Transparent struct types can be tested for equality in a check-expect and the contents of a transparent struct value will be printed in the REPL. While there are good software engineering principles for making types opaque, we will always use transparent structs in this course.

The define-struct definition defines a new type named Name. It also generates the definitions of a bunch of operations on the struct type. For example, the definition of Posn generates functions with the following types:

You may notice that the type of Posn? has three parts (Any, Boolean, and Posn). The first two are the same as any other function type and indicate that the predicate takes any value and returns a boolean. The third part, after the :, is a filter that tells the typechecker two things:

Predicates for all built-in types are annotated with similar filters that allow the type system to reason about predicate checks. This mechanism is called occurrence typing and allows functions, such as the following, to typecheck:

since the typechecker knows that p has type Posn in the ‘then’ branch of the if. This mechanism is restricted to arguments that are variables; testing the result of an expression and then expecting the

Union types provide a mechanism to define a type that is one of several distinct choices. For example, we might define a representation of colored circles, where the available colors are red, green, or blue. We can use symbols to represent the distinct colors; i.e., 'red, 'green, and 'blue. A symbol in Typed Racket is its own type, as illustrated by the following code snippet:

This kind of type is called a singleton type, since it is a type that has exactly one value. By unioning multiple singleton types, we can describe enumeration types. For example, our color type is the union of 'red, 'green, and 'blue. Two other useful singleton types are #t and #f (as one might guess, Boolean is the union of #t and #f).

We can define a function that maps colors to their names as follows:

Here the identifier U in the type stands for union. Also notice that the declared type of color-to-string guarantees that the else clause of the conditional will always be green.

Our definition of colored circles is as follows:

Now we can define a blue unit circle centered at (2, 3) as follows:

We can also define unions of all kinds of types. For example, we might a representation of colored rectangles:

and then define a function for getting the color from a shape

This function is an example of the use of occurrence typing in a conditional. In the first clause of the conditional, the Circle? predicate determines that the shape variable has the type Color in the expression part and does not have that type in the rest of the conditional. Because the typechecker knows that the variable shape must be either a Circle or a Rect, it knows that the type of shape must be Rect in the else clause.

Since type expressions can get quite large and complicated, it is helpful to introduce names for such types. This objective fits nicely with the concept of a data definition that is introduced in the textbook (Section 6.4).

For example, instead of writing

we can give an explicit definition using the define-type construct

We can also give a name to our shape type:

Union types give rise to a notion of subtyping; i.e., the idea that one type is contained in another. For example, the type 'red is contained in the type Color, so we say that 'red is a subtype of Color. Intuitively, you can think of subtyping in Typed Racket as corresponding to the subset relation of the sets of values in the types. For example, the value 'red is contained in the set of Color values {'red, 'green, 'blue}.

Another example of subtyping that you have already experienced is the hierarchy of numeric types. The type Natural is a subtype of Integer, Integer is a subtype of Exact-Rational, etc.

Subtyping comes into play when Typed Racket checks the types of arguments against the type of a function in an application. If an argument expression has a type that is a subtype of the expected type, then it is okay. For example, when checking the expression

we have an argument of type 'red, which is a subtype of the expected type.

As conditional expressions are written with cond, pattern matching expressions are written with match. A match expression has the following general form:

Match evaluation is similar to cond evaluation. First the expression exp_0 is evaluated to a value we’ll call v. Then v is compared against each pattern in turn, in the order given: pat_1, then pat_2, and so on, up to pat_k. If v matches pat_1, then the value of the whole expression is exp_1, and evaluation within the match goes no further. If pat_1 doesn’t match, then v is checked against pat_2, and the value is exp_2. Evaluation continues from pattern to pattern until a match is found (or none is).

Consider this match expression:

In this case, (+ 1 1) is evaluated to 2. This is compared first against the first pattern in order, which is a constant pattern 2. This is a match, so the value of the whole expression is the string "A". With the following alteration, the value of the expression is "B":

There are many useful kinds of patterns besides constant patterns: one such kind is variable patterns. A variable pattern consists of a variable name, and a) always succeeds and b) gives a name to the value matched. Consider this example:

The value of this expression is 31. Why? The expression immediately following match evaluates to 30. Then 30 is compared against the variable pattern n, which succeeds in matching (as variable patterns always do) and furthermore binds the name n to the expression’s value. When the expression (+ n 1) is evaluated, n is bound to 30, and we finally arrive at 31.

Because variable patterns always match, they can be used as catch-all or default patterns in a pattern match, playing a role not entirely unlike what else does in the last branch of a cond. For example:

In this expression, the match of evaluated 17 against the constant pattern 0 fails. The match against n necessarily succeeds, and the value of the expression altogether is the string "not zero".

The variable pattern n in the last example is a suitable candidate for a wildcard pattern, written with the underscore character _. Recall that a variable pattern both matches a value and binds a name to it, but in this case (and many cases in practice) the name is not needed, since n is not subsequently used. In such cases as this, a wildcard pattern, informally known as a "don’t care" pattern, is a good choice. A wildcard pattern always succeeds in matching, like a variable pattern does, but doesn’t bind; that is, it associates no name with the matched value.

The underscore serves not only to catch any expression that falls past the constant pattern 0, but it also expresses clearly that the particular value of the matching expression is of no interest, only the fact that it did not match any previous pattern.

Matching against structures is a convenient way to, first, identify the particular struct under consideration, and also to name the individual components in the structure and thereby eliminate calls to selectors.

Define a point in 2-space as follows:

Now assume there exists an expression of type Point bound to a variable p, and consider the following match:

This expression performs the (admittedly contrived) operation of adding together the x and y components of the point p. The pattern (Point x y) serves several purposes: Point ensures that p is actually a Point struct, and furthermore the names x and y are bound to its two components. Syntactically, this is a real bargain, although it will take practice and experience to appreciate why. Without pattern matching, a similar expression looks like this:

On the whole, the latter expression is no longer (in number of characters) than the first; however, in the part of the expression where the action is — namely, where x and y are added together — the former expression is a clean (+ x y), while the latter is cluttered up with selectors (Point-x and Point-y). Pattern matching often has this clarifying effect by separating the deconstruction of a compound value from computing with its elements.

Using nested patterns with nested structures pushes the advantages of structure matching still further. Consider a line segment structure containing two points as follows:

Now we consider the following (contrived) computation: to subtract the product of the segments y components from the product of its x components. We can write the expression with nested patterns like this:

Compare that expression to this one that uses selectors:

In the second expression, the selectors overwhelm the syntax and make reading the expression (comparatively) difficult; the matched alternative above (- (* ax bx) (* ay by)) is crystal clear by comparison.

Pattern matching is especially useful in the definition of functions. Here is a function definition using only selectors:

When we rewrite the function using a match, the code is not shorter, but its main expression is free of selectors and hence clearer:

With nested structures, nested pattern matching cleans up and clarifies the computation to an even greater extent. The following two functions compute the same property of a line segment; compare the syntax of one to the other.

Recall the definition of the Shape type from above.

We can use pattern matching to write functions that work over union types like Shape. For example, the shape-color function can be written using pattern matching as

We use wild cards for the parts of the shapes that we are not interested in.

Typed Racket also provides a mechanism for matching against multiple values with multiple patterns. For example, say we wanted a function to test if two shapes are the same shape and color. We could write that as

You have to be careful to avoid using the identifiers true, false, empty in patterns. These identifiers are variables (not literals), which means that they will match any value. For example, the following function will always return false.

The correct way to write it is to use the #f and #t literals in the patterns:

Suppose that we want to have lists of shapes?

Informally, we might think of a list of shapes as being either - an empty list - a pair of a shape and a list of shapes

This is an example of an inductively defined set. We can define such sets in Typed Racket as follows:

The Shape-List type is an example of an inductive type. I.e., a type that is defined by one or more base cases (e.g., 'empty-shape-list) and one or more inductive cases (e.g., make-Shape-List).

Inductive types are naturally processed by recursive functions. When writing recursive functions over inductive types, we usually follow a standard pattern of base cases for the base cases in the type defintiion and recursive cases for the inductive cases in the type definition. For example, say we want to write a recursive function to count the number of shapes in a list. We start with the header and a skeleton:

We then add a clause to the match for our base case: the empty list, which has length 0:

We also need a recursive case for the non-empty list. In that situation, the length of the list will be one plus the length of the rest of the list. The complete function is

Sometimes it is necessary to instantiate a polymorphic function at a specific type. We use the inst special form to do this operation. The syntax is

where id is the polymorphic function and the ty1, ty2, … are type arguments (one per variable in id's type). For example, we can instantiate the type of swap by giving it two type arguments:

Typed Racket provides various standard operations on lists as polymorphic functions. We can compute the length of a list with

Reverse the order of a list using

Two or more lists can be concatenated using the append function.

We can extract an element from a list by its index using

Notice that indexing starts at 0. Specifying a negative index or one that is too large results in an error. Lastly, the make-list function creates a list of the given length

Typed Scheme provides a number of higher-order functions that operate on lists:

Local definitions provide two important features:

The syntax of a local definition is

where definitions appear between the curly braces and the expr is evaluated to produce the result. For example:

Locals can also be used to define helper functions (including their type contracts). For example, here is a tail recursive version of the factorial function written using a helper.

Notice that the fact-aux function references n, which is bound as a parameter to the outer function fact. This is an example of using lexical scoping to avoid needing extra parameters to the helper function.

The lambda expression provides a way to define a non-recursive function without giving it a name. The basic syntax is

where the param-+i are the function parameters with the corresponding declared types. Anonymous functions are particularly useful in combination with higher-order functions, such as +map and foldl. For example, we can compute the sum of the squares of a list of numbers as follows

Lambda expressions are also quite useful for writing curried functions. For example, a curried form of addition can be written as

Curried functions are useful when combined with other higher-order functions. For example, using curried-add, we can use map to increment the elements of a list by some amount:

The basic operation for updating a mutable vector is

The Void return type means that this function does not return any value.

With operations, such as vector=-set!, that return Void, our code will often become a sequence of updates. We use the expression form

for this purpose; it has the effect of executing exp1, exp2, … in turn. Its result is the value of expn. For example, we can use it to define a function that swaps two elements of a vector:

Sometimes we need an expression of type Void (e.g., to make the types of a conditional match). We can use the void function, which takes no arguments, for this purpose:

For example, the following expression swaps the +i+th and +j+th elements of a vector when the +i+th element is greater than the +j+th.

In addition to mutable vectors, we will also use mutable structs. These are defined by adding the #:mutable option to the struct definition as in the following example:

When we include the #:mutable option in a struct declaration, Typed Racket will generate additional functions for modifying the struct (one for each declared field). In our Pt example, we get two additional operations.

that can be used to update in place the x and y fields of the struct. For example, here is a function that moves a point by the given offsets.

We only use simple input/output (I/O) operations in this class. Typed Racket provides a function for reading a line of text from the user.

This function returns either a string of the input text or the special EOF (end of file) value. You can use eof-object? to test for EOF.

The display function will write any type of value to the screen.

Since display does not force a newline after its output, you can use the newline function to force a linebreak.

We can combine display and newline together to implement a helpful debugging function.

This function displays its argument and returns it, which means that you can wrap it around any expresssion to see what the result of the expression is.