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 dynamic 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, errors that will be triggered only when they are run, are not 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 just a comment. Returning to our sq function, we would write it in Typed Racket as follows:

#lang typed/racket

(: 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. 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).

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

Even before we try to use this program with specific inputs, we will receive an error message because Typed Racket will notice that it attempts to use the sq function inappropriately (on one too many arguments).

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 of integers).

  • 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.)

  • 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* and '*red are all examples of symbols. While superficially similar to strings, symbols require significantly less internal storage than strings, and in general are more efficient, and are suitable when textual information is helpful but full-fledged strings are not needed.

Function types

Functions in racket and Typed Racket take zero or more arguments and return a single result. We write the type of a function by writing an arrow ->, then the argument types, and then the result type. 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

Note that a function can only ever have one output type, so "where the arrow goes" in the function type is always unambiguous.

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 a type ascription. Type ascriptions are enforced by the Typed Racket compiler, so the programmer who writes them will be held to account for them.

(: 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. First, function types can be written using a prefix notation; e.g.,

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

Typed Racket also supports the following infix function type syntax (please note the extra colon), which is similar to the mapping notations one is accustomed to reading in mathematics:

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