4 Types in Typed Racket

Typed Racket provides a rich variety of types to describe data. This section introduces them.

4.1 Basic Types

The most basic types in Typed Racket are those for primitive data, such as True and False for booleans, String for strings, and Char for characters.

> '"hello, world"

- : String

"hello, world"

> #\f

- : Char

#\f

> #t

- : Boolean [more precisely: True]

#t

> #f

- : False

#f

Each symbol is given a unique type containing only that symbol. The Symbol type includes all symbols.

> 'foo

- : Symbol [more precisely: 'foo]

'foo

> 'bar

- : Symbol [more precisely: 'bar]

'bar

Typed Racket also provides a rich hierarchy for describing particular kinds of numbers.

> 0

- : Integer [more precisely: Zero]

0

> -7

- : Integer [more precisely: Negative-Fixnum]

-7

> 14

- : Integer [more precisely: Positive-Byte]

14

> 3.2

- : Flonum [more precisely: Positive-Float-No-NaN]

3.2

> 7.0+2.8i

- : Float-Complex

7.0+2.8i

Finally, any value is itself a type:

> (ann 23 23)

- : Integer [more precisely: 23]

23

4.2 Function Types

We have already seen some examples of function types. Function types are constructed using ->, where the last type is the result type and the others are the argument types. Here are some example function types:

(-> Number Number)

(-> String String Boolean)

(-> Char (Values String Natural))

The first type requires a Number as input, and produces a Number. The second requires two arguments. The third takes one argument, and produces multiple values, of types String and Natural. Here are example functions for each of these types.

> (lambda ([x : Number]) x)

- : (-> Number Number)

#<procedure>

> (lambda ([a : String] [b : String]) (equal? a b))

- : (-> String String Boolean)

#<procedure>

> (lambda ([c : Char]) (values (string c) (char->integer c)))

- : (-> Char (values (String : (Top | Bot)) (Index : (Top | Bot))))

#<procedure>

4.3 Types for Functions with Optional or Keyword Arguments

Racket functions often take optional or keyword arguments in addition to standard mandatory arguments. Types for these functions can be written concisely using the ->* type constructor. Here are some examples:

(->* () (Number) Number)

(->* (String String) Boolean)

(->* (#:x Number) (#:y Number) (values Number Number))

The first type describes a function that has no mandatory arguments, one optional argument with type Number, and returns a Number.

The second requires two mandatory arguments, no optional arguments, and produces a Boolean. This function type could have been written using -> as (-> String String Boolean).

The third requires a mandatory keyword argument with the keyword #:x and accepts an optional argument with keyword #:y. The result is two values of type Number.

4.4 Union Types

Sometimes a value can be one of several types. To specify this, we can use a union type, written with the type constructor U.

> (let ([a-number 37])     (if (even? a-number)         'yes         'no))

- : Symbol [more precisely: (U 'no 'yes)]

'no

Any number of types can be combined together in a union, and nested unions are flattened.

(U Number String Boolean Char)

4.5 Recursive Types

Recursive types are types whose definitions refer to themselves. This allows a type to describe an infinite family of data. For example, this is the type of binary trees of numbers.

Recursive types can also be created anonymously without the use of define-type using the Rec type constructor.

(define-type BinaryTree (U Number (Pair BinaryTree BinaryTree)))

Types can also be mutually recursive. For example, the above type defintion could also be written like this.

(define-type BinaryTree (U BinaryTreeLeaf BinaryTreeNode))

(define-type BinaryTreeLeaf Number)

(define-type BinaryTreeNode (Pair BinaryTree BinaryTree))

Of course, types which directly refer to themselves are not permitted. For example, both of these definitions are illegal.

> (define-type BinaryTree BinaryTree)

eval:18:0: Type Checker: Error in macro expansion -- parse

error in type;

recursive types are not allowed directly inside their

definition

in: BinaryTree

> (define-type BinaryTree (U Number BinaryTree))

eval:19:0: Type Checker: Error in macro expansion -- parse

error in type;

recursive types are not allowed directly inside their

definition

in: BinaryTree

4.6 Structure Types

Using struct introduces new types, distinct from any previous type.

(struct point ([x : Real] [y : Real]))

Instances of this structure, such as (point 7 12), have type point.

If a struct supertype is provided, then the newly defined type is a subtype of the parent.

4.7 Subtyping

In Typed Racket, all types are placed in a hierarchy, based on what values are included in the type. When an element of a larger type is expected, an element of a smaller type may be provided. The smaller type is called a subtype of the larger type. The larger type is called a supertype. For example, Integer is a subtype of Real, since every integer is a real number. Therefore, the following code is acceptable to the type checker:

(: f (-> Real Real))

(define (f x) (* x 0.75))

(: x Integer)

(define x -125)

(f x)

All types are subtypes of the Any type.

The elements of a union type are individually subtypes of the whole union, so String is a subtype of (U String Number). One function type is a subtype of another if they have the same number of arguments, the subtype’s arguments are more permissive (is a supertype), and the subtype’s result type is less permissive (is a subtype). For example, (-> Any String) is a subtype of (-> Number (U String #f)).

4.8 Polymorphism

Typed Racket offers abstraction over types as well as values. This allows the definition of functions that use parametric polymorphism.

4.8.1 Polymorphic Data Structures

Virtually every Racket program uses lists and other collections. Fortunately, Typed Racket can handle these as well. A simple list processing program can be written like this:

#lang typed/racket

(: sum-list (-> (Listof Number) Number))

(define (sum-list l)

(cond [(null? l) 0]

[else (+ (car l) (sum-list (cdr l)))]))

This looks similar to our earlier programs — except for the type of l, which looks like a function application. In fact, it’s a use of the type constructor Listof, which takes another type as its input, here Number. We can use Listof to construct the type of any kind of list we might want.

We can define our own type constructors as well. For example, here is an analog of the Maybe type constructor from Haskell:

#lang typed/racket

(struct None ())

(struct (a) Some ([v : a]))

(define-type (Opt a) (U None (Some a)))

(: find (-> Number (Listof Number) (Opt Number)))

(define (find v l)

(cond [(null? l) (None)]

[(= v (car l)) (Some v)]

[else (find v (cdr l))]))

The first struct: defines None to be a structure with no contents.

The second definition

(struct (a) Some ([v : a]))

creates a parameterized type, Some, which is a structure with one element, whose type is that of the type argument to Some. Here the type parameters (only one, a, in this case) are written before the type name, and can be referred to in the types of the fields.

The find function takes a number v and list, and produces (Some v) when the number is found in the list, and (None) otherwise. Therefore, it produces a (Opt Number), just as the annotation specified.

4.8.2 Polymorphic Functions

Sometimes functions over polymorphic data structures only concern themselves with the form of the structure. For example, one might write a function that takes the length of a list of numbers:

#lang typed/racket

(: list-number-length (-> (Listof Number) Integer))

(define (list-number-length l)

(if (null? l)

0

(add1 (list-number-length (cdr l)))))

and also a function that takes the length of a list of strings:

#lang typed/racket

(: list-string-length (-> (Listof String) Integer))

(define (list-string-length l)

(if (null? l)

0

(add1 (list-string-length (cdr l)))))

Notice that both of these functions have almost exactly the same definition; the only difference is the name of the function. This is because neither function uses the type of the elements in the definition.

We can abstract over the type of the element as follows:

#lang typed/racket

(: list-length (All (A) (-> (Listof A) Integer)))

(define (list-length l)

(if (null? l)

0

(add1 (list-length (cdr l)))))

The new type constructor All takes a list of type variables and a body type. The type variables are allowed to appear free in the body of the All form.

4.8.3 Lexically Scoped Type Variables

When the : type annotation form includes type variables for parametric polymorphism, the type variables are lexically scoped. In other words, the type variables are bound in the body of the definition that you annotate.

For example, the following definition of my-id uses the type variable a to annotate the argument x:

(: my-id (All (a) (-> a a)))

(define my-id (lambda ([x : a]) x))

Lexical scope also implies that type variables can be shadowed, such as in the following example:

(: my-id (All (a) (-> a a)))

(define my-id

(lambda ([x : a])

(: helper (All (a) (-> a a)))

(define helper

(lambda ([y : a]) y))

(helper x)))

The reference to a inside the inner lambda refers to the type variable in helper’s annotation. That a is not the same as the a in the annotation of the outer lambda expression.

4.9 Variable-Arity Functions: Programming with Rest Arguments

Typed Racket can handle some uses of rest arguments.

4.9.1 Uniform Variable-Arity Functions

In Racket, one can write a function that takes an arbitrary number of arguments as follows:

#lang racket

(define (sum . xs)

(if (null? xs)

0

(+ (car xs) (apply sum (cdr xs)))))

(sum)

(sum 1 2 3 4)

(sum 1 3)

The arguments to the function that are in excess to the non-rest arguments are converted to a list which is assigned to the rest parameter. So the examples above evaluate to 0, 10, and 4.

We can define such functions in Typed Racket as well:

#lang typed/racket

(: sum (-> Number * Number))

(define (sum . xs)

(if (null? xs)

0

(+ (car xs) (apply sum (cdr xs)))))

This type can be assigned to the function when each element of the rest parameter is used at the same type.

4.9.2 Non-Uniform Variable-Arity Functions

However, the rest argument may be used as a heterogeneous list. Take this (simplified) definition of the R6RS function fold-left:

#lang racket

(define (fold-left f i as . bss)

(if (or (null? as)

(ormap null? bss))

i

(apply fold-left

f

(apply f i (car as) (map car bss))

(cdr as)

(map cdr bss))))

(fold-left + 0 (list 1 2 3 4) (list 5 6 7 8))

(fold-left + 0 (list 1 2 3) (list 2 3 4) (list 3 4 5) (list 4 5 6))

(fold-left (λ (i v n s) (string-append i (vector-ref v n) s))

""

(list (vector "A cat" "A dog" "A mouse")

(vector "tuna" "steak" "cheese"))

(list 0 2)

(list " does not eat " "."))

Here the different lists that make up the rest argument bss can be of different types, but the type of each list in bss corresponds to the type of the corresponding argument of f. We also know that, in order to avoid arity errors, the length of bss must be two less than the arity of f. The first argument to f is the accumulator, and as corresponds to the second argument of f.

The example uses of fold-left evaluate to 36, 42, and "A cat does not eat cheese.".

In Typed Racket, we can define fold-left as follows:

#lang typed/racket

(: fold-left

(All (C A B ...)

(-> (-> C A B ... B C) C (Listof A) (Listof B) ... B

C)))

(define (fold-left f i as . bss)

(if (or (null? as)

(ormap null? bss))

i

(apply fold-left

f

(apply f i (car as) (map car bss))

(cdr as)

(map cdr bss))))

Note that the type variable B is followed by an ellipsis. This denotes that B is a dotted type variable which corresponds to a list of types, much as a rest argument corresponds to a list of values. When the type of fold-left is instantiated at a list of types, then each type t which is bound by B (notated by the dotted pre-type t ... B) is expanded to a number of copies of t equal to the length of the sequence assigned to B. Then B in each copy is replaced with the corresponding type from the sequence.

So the type of (inst fold-left Integer Boolean String Number) is

(-> (-> Integer Boolean String Number Integer) Integer (Listof Boolean) (Listof String) (Listof Number) Integer).