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.

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-lambda (-> 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: Expected Number, but got String in:

(quote "not a 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.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 not be recursive.