3 Specifying Types

The previous section introduced the basics of the Typed Racket type system. In this section, we will see several new features of the language, allowing types to be specified and used.

3.1 Type Annotation and Binding Forms

In general, variables in Typed Racket must be annotated with their type. A later subsection (When do you need type annotations?) introduces a heuristic which more precisely details when type annotations are needed.

3.1.1 Annotating Definitions

We have already seen the : type annotation form. This is useful for definitions, at both the top level of a module

(: x Number)

(define x 7)

and in an internal definition

(let ()

(: x Number)

(define x 7)

(add1 x))

In addition to the : form, almost all binding forms from racket have counterparts which allow the specification of types. The define: form allows the definition of variables in both top-level and internal contexts.

(define: x : Number 7)

(define: (id [z : Number]) : Number z)

Here, x has the type Number, and id has the type (-> Number Number). In the body of id, z has the type Number.

3.1.2 Annotating Local Binding

(let: ([x : Number 7])

(add1 x))

The let: form is exactly like let, but type annotations are provided for each variable bound. Here, x is given the type Number. The let*: and letrec: are similar. Annotations are optional with let: and variants.

(let-values: ([([x : Number] [y : String]) (values 7 "hello")])

(+ x (string-length y)))

The let*-values: and letrec-values: forms are similar.

3.1.3 Annotating Functions

Function expressions also bind variables, which can be annotated with types. This function expects two arguments, a Number and a String:

(lambda: ([x : Number] [y : String]) (+ x 5))

This function accepts at least one String, followed by arbitrarily many Numbers. In the body, y is a list of Numbers.

(lambda: ([x : String] . [y : Number *]) (apply + y))

This function has the type (-> String Number * Number). Functions defined by cases may also be annotated:

(case-lambda: [() 0]

[([x : Number]) x])

This function has the type (case-> (-> Number) (-> Number Number)).

3.1.4 Annotating Single Variables

When a single variable binding needs annotation, the annotation can be applied to a single variable using a reader extension:

(let ([#{x : Number} 7]) (add1 x))

This is equivalent to the earlier use of let:. This is especially useful for binding forms which do not have counterparts provided by Typed Racket, such as let+:

(let+ ([val #{x : Number} (+ 6 1)])

(* x x))

3.1.5 Annotating Expressions

It is also possible to provide an expected type for a particular expression.

(ann (+ 7 1) Number)

This ensures that the expression, here (+ 7 1), has the desired type, here Number. Otherwise, the type checker signals an error. For example:

> (ann "not a number" Number)

eval:2:0: Type Checker: type mismatch

expected: Number

given: String

in: Number

3.2 Type Inference

In many cases, type annotations can be avoided where Typed Racket can infer them. For example, the types of all local bindings using let and let* can be inferred.

(let ([x 7]) (add1 x))

In this example, x has the type Exact-Positive-Integer.

Similarly, top-level constant definitions do not require annotation:

(define y "foo")

In this examples, y has the type String.

Finally, the parameter types for loops are inferred from their initial values.

(let loop ([x 0] [y (list 1 2 3)])

(if (null? y) x (loop (+ x (car y)) (cdr y))))

Here x has the inferred type Integer, and y has the inferred type (Listof Integer). The loop variable has type (-> Integer (Listof Integer) Integer).

3.2.1 When do you need type annotations?

The last several subsections explained several ways to add type annotations and explained that type inference allows some annotations to be left out. Since annotations can often be omitted, it is helpful to know the situations in which they are actually required.

The following four rules of thumb will usually suffice to determine if a type annotation is necessary.

An expression or definition needs a type annotation if it:

• is a define form for a function,

• is a lambda that is immediately bound to a variable,

• is a lambda that is an argument to a polymorphic function, or

• is defining a mutable variable.

Here are examples that correspond to each of the cases above:

In all four cases, if the type annotation is omitted then the inferred type will often be too conservative (e.g., Any) and the code may not type-check.

3.3 New Type Names

Any type can be given a name with define-type.

(define-type NN (-> Number Number))

Anywhere the name NN is used, it is expanded to (-> Number Number). Type names may be recursive or even mutually recursive.