Typed Racket provides a rich variety of types to describe data. This section introduces them.
> '"hello, world"
- : String
- : Char
- : True
- : False
Each symbol is given a unique type containing only that symbol. The Symbol type includes all symbols.
- : 'foo
- : 'bar
Typed Racket also provides a rich hierarchy for describing particular kinds of numbers.
- : Integer [more precisely: Zero]
- : Integer [more precisely: Negative-Fixnum]
- : Integer [more precisely: Positive-Byte]
- : Flonum [more precisely: Positive-Float-No-NaN]
- : Float-Complex
Finally, any value is itself a type:
> (ann 23 23)
- : Integer [more precisely: 23]
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:
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)
> (lambda ([a : String] [b : String]) (equal? a b))
- : (-> String String Boolean)
> (lambda ([c : Char]) (values (string c) (char->integer c)))
- : (-> Char (values (String : (Top | Bot)) (Index : (Top | Bot))))
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 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.
Sometimes a value can be one of several types. To specify this, we can use a union type, written with the type constructor U.
Any number of types can be combined together in a union, and nested unions are flattened.
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, all recursive types must pass the contractivity check. In other words, types which directly refer to themselves are not permitted. They must be used as arguments to productive type constructors, such as Listof and Pairof. For example, of the following definitions, only the last is legal.
> (define-type BinaryTree BinaryTree)
eval:18:0: Type Checker: Error in macro expansion -- parse
error in type;
not in a productive position
> (define-type BinaryTree (U Number BinaryTree))
eval:19:0: Type Checker: Error in macro expansion -- parse
error in type;
not in a productive position
> (define-type BinaryTree (U Number (Listof BinaryTree)))
Using struct introduces new types, distinct from any previous type.
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.
> (: prop:foo (Struct-Property (-> Self Number))) > (: foo-pred (-> Any Boolean : (Has-Struct-Property prop:foo)))
> (: foo-accessor (-> (Has-Struct-Property prop:foo) (Some (X) (-> X Number) : #:+ X)))
> (define-values (prop:foo foo-pred foo-accessor) (make-struct-type-property 'foo))
Struct-Property creates a type for a structure type property descriptor and its argument is the expected type for property values. In particular, when a structure type property expects a function to be applied with the receiver, a structure instance the property value is extracted from, Self is used to denotes the receiver type. For a value in supplied in a struct definition for such a property, we use the structure type for a by-position parameter for Self:
A property predicate tells the arguments variable is a Has-Struct-Property if the predicate check succeeds. Has-Struct-Property describes a subtyping relation between structure types and properties attached to them. In the example above, apple is a subtype of (Has-Struct-Property prop:foo)
For a property accessor procedure, the argument must have a Has-Struct-Property type. If a property expects a value to be a function called with the receiver, i.e. Self appears in the type of the corresponding property descriptor, an existential type result is required. Its quantifier needs to correspond to Self and also appear in the proposition. Such a return type ensures that the extracted function cannot be called with another instance of the structure type or substructure types other than the receiver:
> (let ([a1 : apple (apple 42)]) ((foo-accessor a1) a1))
- : Number
> (let ([a1 : apple (apple 42)]) ((foo-accessor a1) (apple 10)))
eval:27:0: Type Checker: type mismatch
Otherwise, the return type should be the same as the type argument to Struct-Property for the descriptor.
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:
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)).
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 —
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
creates a type constructor, Some, and defines a namesake 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.
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)))))
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:
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)))
Typed Racket can handle some uses of rest arguments.
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.
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.