An example

Racket (as opposed to Typed Racket) is a dynamically typed language, which means that type errors are not detected until the erroneous code is actually executed. For example, in Racket, we might define a function for squaring numbers like so:

;; sq : Number -> Number
;; return the square of a number
;;
(define (sq x)
  (* x x))

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

> (sq 1 2)
sq: expects only 1 argument, but found 2
> (sq "hi")
*: expects a number as 1st argument, given "hi"

In this simple example, waiting until we run the program to find the error is not a big deal, but in larger programs such errors can be hidden from immediate detection. Suffice it to say that programs that contain undetected errors are something like ticking time bombs. For example, consider the following (erroneous) function

;; f : Boolean Number Number -> Number
;;
(define (f flg a b)
  (cond
    [flg (sq a b)] ;; type error: sq should be applied only to one argument
    [else 1]))

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

> (f #f 1 2)
1

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 actual code, instead of as just a comment. Returning to our sq function, we would write it in Typed Racket as follows:

#lang typed/racket

(require "../include/uchicago151.rkt")

(: sq : Number -> Number)
;; return the square of a number
;;
(define (sq x)
  (* x x))

The very 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. Following that is a require expression that customizes Typed Racket for this course. This line will also be included in all of your programs. Following that is the definition of the sq function. The definition 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 (i.e., a function from Number to Number).

The buggy function f from above is now written in Typed Racket as follows:

(: f : Boolean Number Number -> Number)
;; test program
;;
(define (f flg a b)
  (cond
    [flg (sq a b)]
    [else 1]))

But when we compile this function, we will receive a type error message because Typed Racket will notice that the use of sq has too many arguments.

Type Checker: could not apply function;
 wrong number of arguments provided
  expected: 1
  given: 2 in: (sq a b)

Basic types

Typed Racket defines a very large collection of basic types. We will only use a small subset of them in this course.

Numbers

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

  • Integer

    is the type of the integers.

  • Exact-Rational

    is the type of the rational numbers (i.e., numbers that can be written as a fraction).

  • Real

    is the type of the real numbers. Computer representations of the reals are necessarily inexact because real numbers can require infinite precision to represent, but computers use finite amounts of storage to hold their values.

  • Number

    is the type of all numbers, including complex numbers.

Other basic types

  • Boolean

    is the type of logical values. There are exactly two of these; we write them #t and #f. (They may also be written true and false, but, as we will see later, #t and #f are to be prefered.)

  • String

    is the type of strings of characters, i.e., text, and are enclosed in double quotes, as in "chocolate" and "vanilla".

  • Symbol

    is the type of symbols, which are sequences of characters preceded by a single quotation mark. For example, 'red, 'red*, '*, 'abc-def, and '+abc are all symbols. While superficially similar to strings, symbols require significantly less internal storage than strings, are more efficient, and are suitable when textual information is helpful but full-fledged strings are not needed.

Function types

Functions in Typed Racket (and 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: For example, the type of a function that consumes an Integer and produces a String is written

Integer -> String

The type of a function that consumes an Integer and a Boolean and produces a String is written like this:

Integer Boolean -> String

Typed Racket also supports a prefix syntax for functions types that is more Scheme-like. In this alternate notation, we write the ->, then the argument types, and then the result type. Using this syntax, the previous examples are written

-> Integer String

-> Integer Boolean String

Note that a function can only ever have one output type, so "where the arrow goes" when using the prefix notation is always unambiguous. While this syntax is more in keeping with the syntax of Racket, we prefer the infix syntax as it matches the syntax of type contracts in the text book and is easier to read.

Type annotations

We can declare the type of a variable using the syntax

(: name : type)

This explicit association, in code, between a name and a type is called type ascription (or sometimes a type annotation). Type ascriptions are checked by the Typed Racket compiler.

(: n : Integer)

Having asserted that n must be an Integer, the program is allowed only to bind n to values of type Integer.

Typed Racket accepts a number of different syntaxes for types and type annotations. As noted above, function types can be written using a prefix notation; e.g.,

(: sq : -> Number Number)
(: f : -> Boolean Number Number Number)

One can also leave off the second ":", but in that case function types need an extra set of parentheses.

(: n Integer)
(: sq (-> Number Number))
(: f (Boolean Number Number -> Number))