Version: 5.1.1
The Typed Racket Reference
1 Type Reference
Any Racket value. All other types are subtypes of
Any.
The empty type. No values inhabit this type, and
any expression of this type will not evaluate to a value.
1.1 Base Types
1.1.1 Numeric Types
These types represent the hierarchy of
numbers of Racket.
Integer includes only
integers that are
exact
numbers, corresponding to the predicate
exact-integer?.
"Real" includes both exact and inexact reals.
An
"Inexact-Real" can be either 32- or 64-bit floating-point
numbers.
"Float" is restricted to 64-bit floats, which are the
default in Racket.
Examples: |
> 7 | - : Positive-Byte | 7 | > 8.3 | - : Positive-Float | 8.3 | > (/ 8 3) | - : Positive-Exact-Rational | 8/3 | > 0 | - : Zero | 0 | > -12 | - : Negative-Fixnum | -12 | > 3+4i | - : Exact-Number | 3+4i |
|
1.1.2 Other Base Types
These types represent primitive Racket data.
1.2 Singleton Types
Some kinds of data are given singleton types by default. In
particular, symbols and keywords have types which
consist only of the particular symbol or keyword. These types are
subtypes of Symbol and Keyword, respectively.
Examples: |
> '#:foo | - : #:foo | '#:foo | > 'bar | - : 'bar | 'bar |
|
1.3 Containers
The following base types are parameteric in their type arguments.
is the
pair containing
s as the
car
and
t as the
cdrExamples: |
> (cons 1 2) | - : (Pairof One Positive-Byte) | '(1 . 2) | > (cons 1 "one") | - : (Pairof One String) | '(1 . "one") |
|
is the type of the list with one element, in order,
for each type provided to the
List type constructor.
(List t ... trest ... bound) |
is the type of a list with
one element for each of the
ts, plus a sequence of elements
corresponding to
trest, where
bound
must be an identifier denoting a type variable bound with
....
Examples: |
> (list 'a 'b 'c) | - : (List 'a 'b 'c) | '(a b c) | > (map symbol->string (list 'a 'b 'c)) | - : (Pairof String (Listof String)) | '("a" "b" "c") |
|
Example: |
> (box "hello world") | - : (Boxof String) | '#&"hello world" |
|
Example: |
> #'here | - : (Syntaxof 'here) | #<syntax:27:0 here> |
|
is the type of the list with one element, in order,
for each type provided to the
Vector type constructor.
Examples: |
> (vector 1 2 3) | - : (Vector Integer Integer Integer) | '#(1 2 3) | > #(a b c) | - : (Vector Symbol Symbol Symbol) | '#(a b c) |
|
is the type of a
hash table with key type
k and value type
v.
Example: |
> #hash((a . 1) (b . 2)) | - : (HashTable Symbol Integer) | '#hash((b . 2) (a . 1)) |
|
A
channel on which only
ts can be sent.
A
parameter of
t. If two type arguments are supplied,
the first is the type the parameter accepts, and the second is the type returned.
Example: |
> (delay 3) | - : (Promise Positive-Byte) | #<promise:eval:34:0> |
|
A recursive union containing types traversed by
datum->syntax. Note that this is
not the type produced
by
read.
1.4 Other Type Constructors
(dom ... -> rng) |
(dom ... rest * -> rng) |
(dom ... rest ... bound -> rng) |
(dom -> rng : pred) |
is the type of functions from the (possibly-empty)
sequence
dom ... to the
rng type. The second form
specifies a uniform rest argument of type
rest, and the
third form specifies a non-uniform rest argument of type
rest with bound
bound. In the third form, the
second occurrence of
... is literal, and
bound
must be an identifier denoting a type variable. In the fourth form,
there must be only one
dom and
pred is the type
checked by the predicate.
Examples: |
> (λ: ([x : Number]) x) | - : (Complex -> Complex : ((! False @ 0) | (False @ 0)) (0)) | #<procedure> | > (λ: ([x : Number] y : String *) (length y)) | - : (Complex String * -> Index) | #<procedure> | > ormap | - : (All (a c b ...) ((a b ... b -> c) (Listof a) (Listof b) ... b -> c)) | #<procedure:ormap> | > string? | - : (Any -> Boolean : String) | #<procedure:string?> |
|
is the union of the types
t ....
Example: |
> (λ: ([x : Real])(if (> 0 x) "yes" 'no)) | - : (Real -> (U String 'no) : (Top | Bot)) | #<procedure> |
|
is a function that behaves like all of
the
fun-tys, considered in order from first to last. The
fun-tys must all be function
types constructed with
->.
is the instantiation of the parametric type
t at types
t1 t2 ...
is a parameterization of type
t, with
type variables
v .... If
t is a function type
constructed with
->, the outer pair of parentheses
around the function type may be omitted.
is the type of a sequence of multiple values, with
types
t .... This can only appear as the return type of a
function.
Example: |
> (values 1 2 3) | - : (Values One Positive-Byte Positive-Byte) | 1 | 2 | 3 |
|
where v is a number, boolean or string, is the singleton type containing only that value
where val is a Racket value, is the singleton type containing only that value
where i is an identifier can be a reference to a type
name or a type variable
is a recursive type where n is bound to the
recursive type in the body t
1.5 Other Types
Either t or #f
2 Special Form Reference
Typed Racket provides a variety of special forms above and beyond
those in Racket. They are used for annotating variables with types,
creating new types, and annotating expressions.
2.1 Binding Forms
loop, f, a, and v are names, t is a type.
e is an expression and body is a block.
(let: ([v : t e] ...) . body) |
(let: loop : t0 ([v : t e] ...) . body) |
Local bindings, like
let, each with
associated types. In the second form,
t0 is the type of the
result of
loop (and thus the result of the entire
expression as well as the final
expression in
body).
Type annotations are optional.
|
(let*: ([v : t e] ...) . body) |
|
|
|
|
2.2 Anonymous Functions
(lambda: formals . body) |
|
formals | | = | | ([v : t] ...) | | | | | | ([v : t] ... v : t *) | | | | | | ([v : t] ... v : t ...) |
|
A function of the formal arguments
v, where each formal
argument has the associated type. If a rest argument is present, then
it has type
(Listof t).
An alias for the same form using
lambda:.
A polymorphic function, abstracted over the type variables
a. The type variables a are bound in both the types
of the formal, and in any type expressions in the body.
A function of multiple arities. Note that each formals must have a
different arity.
For the type declaration of
add-map look at
case-lambda.
A polymorphic function of multiple arities.
(opt-lambda: formals . body) |
|
formals | | = | | ([v : t] ... [v : t default] ...) | | | | | | ([v : t] ... [v : t default] ... v : t *) | | | | | | ([v : t] ... [v : t default] ... v : t ...) |
|
A function with optional arguments.
A polymorphic function with optional arguments.
2.3 Loops
(for: type-ann-maybe (for-clause ...) | expr ...+) |
|
|
type-ann-maybe | | = | | | | | | | | : Void | | | | | | for:-clause | | = | | [id : t seq-expr] | | | | | | [id seq-expr] | | | | | | #:when guard |
|
Like
for, but each
id having the associated type
t. Since the return type is always
Void, annotating
the return type of a
for form is optional. Unlike
for, multi-valued
seq-exprs are not supported.
Type annotations in clauses are optional for all
for:
variants.
|
(for/or: : u (for:-clause ...) expr ...+) |
|
These behave like their non-annotated counterparts, with the exception
that #:when clauses can only appear as the last
for:-clause. The last expr of the body must have
type u.
(for/lists: : u ([id : t] ...) | (for:-clause ...) | expr ...+) |
|
|
(for/fold: : u ([id : t init-expr] ...) | (for:-clause ...) | expr ...+) |
|
|
These behave like their non-annotated counterparts. Unlike the above,
#:when clauses can be used freely with these.
(for*: type-ann-maybe (for-clause ...) | expr ...+) |
|
|
(for*/lists: : u ([id : t] ...) | (for:-clause ...) | expr ...+) |
|
|
(for*/fold: : u ([id : t init-expr] ...) | (for:-clause ...) | expr ...+) |
|
|
These behave like their non-annotated counterparts.
(do: : u ([id : t init-expr step-expr-maybe] ...) | (stop?-expr finish-expr ...) | expr ...+) |
|
|
step-expr-maybe | | = | | | | | | | | step-expr |
|
Like
do, but each
id having the associated type
t, and
the final body
expr having the type
u. Type
annotations are optional.
2.4 Definitions
These forms define variables, with annotated types. The first form
defines
v with type
t and value
e. The
second and third forms defines a function
f with appropriate
types. In most cases, use of
: is preferred to use of
define:.
2.5 Structure Definitions
(struct: maybe-type-vars name-spec ([f : t] ...) options ...) |
|
maybe-type-vars | | = | | | | | | | | (v ...) | | | | | | name-spec | | = | | name | | | | | | name parent | | | | | | options | | = | | #:transparent | | | | | | #:mutable |
|
Defines a
structure with the name
name, where the
fields
f have types
t, similar to the behavior of
struct.
When
parent is present, the
structure is a substructure of
parent. When
maybe-type-vars is present, the structure is polymorphic in the type
variables
v.
Options provided have the same meaning as for the struct form.
(define-struct: maybe-type-vars name-spec ([f : t] ...) options ...) |
|
maybe-type-vars | | = | | | | | | | | (v ...) | | | | | | name-spec | | = | | name | | | | | | (name parent) | | | | | | options | | = | | #:transparent | | | | | | #:mutable |
|
2.6 Names for Types
The first form defines
name as type, with the same meaning as
t. The second form is equivalent to
(define-type name (All (v ...) t)). Type names may
refer to other types defined in the same module, but
cycles among them are prohibited.
2.7 Generating Predicates Automatically
Defines
name as a predicate for the type
t.
name has the type
(Any -> Boolean : t).
t may not contain function types.
2.8 Type Annotation and Instantiation
This declares that v has type t.
The definition of v must appear after this declaration. This
can be used anywhere a definition form may be used.
This declares that the vs have
the types t, and also provides all of the vs.
#{v : t} This declares that the variable v has type
t. This is legal only for binding occurrences of v.
Ensure that e has type t, or
some subtype. The entire expression has type t.
This is legal only in expression contexts.
#{e :: t} This is identical to (ann e t).
Instantiate the type of
e with types
t ....
e must have a polymorphic type with the
appropriate number of type variables. This is legal only in expression
contexts.
Examples: |
> (: fold-list : (All (A) (Listof A) -> (Listof A))) | | > (fold-list (list "1" "2" "3" "4")) | - : (Listof String) | '("4" "3" "2" "1") |
|
#{e @ t ...} This is identical to (inst e t ...).
2.9 Require
Here, m is a module spec, pred is an identifier
naming a predicate, and r is an optionally-renamed identifier.
(require/typed m rt-clause ...) |
|
rt-clause | | = | | [r t] | | | | | | [struct name ([f : t] ...)] | | | | | | [struct (name parent) ([f : t] ...)] | | | | | | [opaque t pred] |
|
This form requires identifiers from the module m, giving
them the specified types.
The first form requires r, giving it type t.
The second and third forms require the struct with name name
with fields f ..., where each field has type t. The
third form allows a parent structure type to be specified.
The parent type must already be a structure type known to Typed
Racket, either built-in or via require/typed. The
structure predicate has the appropriate Typed Racket filter type so
that it may be used as a predicate in if expressions in Typed
Racket.
The fourth case defines a new type t. pred, imported from
module m, is a predicate for this type. The type is defined
as precisely those values to which pred produces
#t. pred must have type (Any -> Boolean).
Opaque types must be required lexically before they are used.
In all cases, the identifiers are protected with contracts which
enforce the specified types. If this contract fails, the module
m is blamed.
Some types, notably polymorphic types constructed with All,
cannot be converted to contracts and raise a static error when used in
a require/typed form. Here is an example of using
case-lambda in require/typed.
file-or-directory-modify-seconds has some arguments which are optional.
So we need to use case-lambda.
3 Libraries Provided With Typed Racket
The typed/racket language corresponds to the
racket language—that is, any identifier provided
by racket, such as modulo is available by default in
typed/racket.
The typed/racket/base language corresponds to the
racket/base language.
Some libraries have counterparts in the typed
collection, which provide the same exports as the untyped versions.
Such libraries include srfi/14,
net/url, and many others.
To participate in making more libraries available, please visit
here.
Other libraries can be used with Typed Racket via
require/typed.
4 Utilities
Typed Racket provides some additional utility functions to facilitate typed programming.
Verifies that the argument satisfies the constraint. If no predicate
is provided, simply checks that the value is not
#f.
Examples: |
> (define: x : (U #f Number) (string->number "7")) | > x | - : (U Zero One Byte-Larger-Than-One Positive-Index-Not-Byte Positive-Fixnum-Not-Index Negative-Fixnum Positive-Integer-Not-Fixnum Negative-Integer-Not-Fixnum Positive-Rational-Not-Integer Negative-Rational-Not-Integer Float-Positive-Zero Flonum-Negative-Zero Float-Nan Positive-Float Negative-Float Single-Flonum-Positive-Zero Single-Flonum-Negative-Zero Single-Flonum-Nan Positive-Single-Flonum Negative-Single-Flonum Exact-Number-Not-Real Float-Complex Single-Flonum-Complex False) | 7 | > (assert x) | - : Complex | 7 | > (define: y : (U String Number) 0) | > y | - : (U String Zero One Byte-Larger-Than-One Positive-Index-Not-Byte Positive-Fixnum-Not-Index Negative-Fixnum Positive-Integer-Not-Fixnum Negative-Integer-Not-Fixnum Positive-Rational-Not-Integer Negative-Rational-Not-Integer Float-Positive-Zero Flonum-Negative-Zero Float-Nan Positive-Float Negative-Float Single-Flonum-Positive-Zero Single-Flonum-Negative-Zero Single-Flonum-Nan Positive-Single-Flonum Negative-Single-Flonum Exact-Number-Not-Real Float-Complex Single-Flonum-Complex) | 0 | > (assert y number?) | - : Complex | 0 | > (assert y boolean?) | Assertion failed |
|
Guard the body with assertions. If any of the assertions fail, the
program errors. These assertions behave like
assert.
5 Typed Racket Syntax Without Type Checking
On occasions where the Typed Racket syntax is useful, but actual
typechecking is not desired, the typed/racket/no-check
and typed/racket/base/no-check languages are useful.
They provide the same bindings and syntax as
typed/racket and typed/racket/base,
but do no type checking.
Examples:
6 Typed Regions
The with-type for allows for localized Typed Racket regions in otherwise untyped code.
(with-type result-spec fv-clause body ...+) |
(with-type export-spec fv-clause body ...+) |
|
fv-clause | | = | | | | | | | | #:freevars ([id fv-type] ...) | | | | | | result-spec | | = | | #:result type | | | | | | export-spec | | = | | ([export-id export-type] ...) |
|
The first form, an expression, checks that
body ...+ has the type
type.
If the last expression in
body ...+ returns multiple values,
type must
be a type of the form
(values t ...).
Uses of the result values are appropriately checked by contracts generated from
type.
The second form, which can be used as a definition, checks that each of the export-ids
has the specified type. These types are also enforced in the surrounding code with contracts.
The ids are assumed to
have the types ascribed to them; these types are converted to contracts and checked dynamically.
Examples: |
> (with-type #:result Number 3) | 3 | | contract violation: expected <Number>, given: #f | contract from (region typed-region), blaming top-level | contract: (-> Number Number) | | "hello, world" | | self-contract violation: expected <String>, given: 'hello | contract on x from top-level, blaming top-level | contract: String | at: eval:5.0 | | > (fun val) | 17 |
|
7 Optimization in Typed Racket
See
Optimization in Typed Racket
in the guide for tips to get the most out of the optimizer.
Typed Racket provides a type-driven optimizer that rewrites well-typed
programs to potentially make them faster. It should in no way make
your programs slower or unsafe.
Typed Racket’s optimizer is turned on by default. If you want to
deactivate it (for debugging, for instance), you must add the
#:no-optimize keyword when specifying the language of your
program:
#lang typed/racket #:no-optimize
8 Legacy Forms
The following forms are provided by Typed Racket for backwards
compatibility.
Equivalent to the
language.