2 Special Form Reference

6.0.1

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 var are names, type is a type. e is an expression and body is a block.

syntax
(let maybe-tvars (binding ...) . body)
(let loop maybe-ret (binding ...) . body)

binding = [var e]
| [var : type e]

maybe-tvars =
| #:forall (tvar ...)
| #:∀ (tvar ...)

maybe-ret =
| : type0

Local bindings, like let, each with associated types. In the second form, type0 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.

Examples:

> (: filter-even : (-> (Listof Natural) (Listof Natural) (Listof Natural)))
> (define (filter-even lst accum)
    (if (null? lst)
        accum
        (let ([first : Natural (car lst)]
              [rest  : (Listof Natural) (cdr lst)])
              (if (even? first)
                  (filter-even rest (cons first accum))
                  (filter-even rest accum)))))
> (filter-even (list 1 2 3 4 5 6) null)
- : (Listof Nonnegative-Integer)
'(6 4 2)

Examples:

> (: filter-even-loop (-> (Listof Natural) (Listof Natural)))
> (define (filter-even-loop lst)
    (let loop : (Listof Natural)
         ([accum : (Listof Natural) null]
          [lst   : (Listof Natural) lst])
         (cond
           [(null? lst)       accum]
           [(even? (car lst)) (loop (cons (car lst) accum) (cdr lst))]
           [else              (loop accum (cdr lst))])))
> (filter-even-loop (list 1 2 3 4))
- : (Listof Nonnegative-Integer)
'(4 2)

If polymorphic type variables are provided, they are bound in the type expressions for variable bindings.

Example:

> (let #:forall (A) ([x : A 0]) x)
- : Integer [more precisely: Zero]
0

syntax
(letrec (binding ...) . body)
syntax
(let* (binding ...) . body)
syntax
(let-values ([(var+type ...) e] ...) . body)
syntax
(letrec-values ([(var+type ...) e] ...) . body)
syntax
(let*-values ([(var+type ...) e] ...) . body)

Type-annotated versions of letrec, let*, let-values, letrec-values, and let*-values. As with let, type annotations are optional.

syntax
(let/cc v : t . body)
syntax
(let/ec v : t . body)

Type-annotated versions of let/cc and let/ec.

2.2 Anonymous Functions

syntax
(lambda maybe-tvars formals maybe-ret . body)

formals = (formal ...)
| (formal ... . rst)

formal = var
| [var default-expr]
| [var : type]
| [var : type default-expr]
| keyword var
| keyword [var : type]
| keyword [var : type default-expr]

rst = var
| [var : type *]
| [var : type ooo bound]

maybe-tvars =
| #:forall (tvar ...)
| #:∀ (tvar ...)
| #:forall (tvar ... ooo)
| #:∀ (tvar ... ooo)

maybe-ret =
| : type

Constructs an anonymous function like the lambda form from racket/base, but allows type annotations on the formal arguments. If a type annotation is left out, the formal will have the type Any.

Examples:

> (lambda ([x : String]) (string-append x "bar"))
- : (-> String String)
#<procedure>
> (lambda (x [y : Integer]) (add1 y))
- : (-> Any Integer Integer)
#<procedure>
> (lambda (x) x)
- : (-> Any Any)
#<procedure>

Type annotations may also be specified for keyword and optional arguments:

Examples:

> (lambda ([x : String "foo"]) (string-append x "bar"))
- : (->* () (String) String)
#<procedure>
> (lambda (#:x [x : String]) (string-append x "bar"))
- : (-> #:x String String)
#<procedure:eval:13:0>
> (lambda (x #:y [y : Integer 0]) (add1 y))
- : (-> Any [#:y Integer] Integer)
#<procedure:eval:14:0>
> (lambda ([x 'default]) x)
- : (->* () (Any) Any)
#<procedure>

The lambda expression may also specify polymorphic type variables that are bound for the type expressions in the formals.

Examples:

> (lambda #:forall (A) ([x : A]) x)
- : (All (A) (-> A A))
#<procedure>
> (lambda #:∀ (A) ([x : A]) x)
- : (All (A) (-> A A))
#<procedure>

In addition, a type may optionally be specified for the rest argument with either a uniform type or using a polymorphic type. In the former case, the rest argument is given the type (Listof type) where type is the provided type annotation.

Examples:

> (lambda (x . rst) rst)
- : (-> Any Any * (Listof Any))
#<procedure>
> (lambda (x rst : Integer *) rst)
- : (-> Any Integer * (Listof Integer))
#<procedure>
> (lambda #:forall (A ...) (x rst : A ... A) rst)
- : (All (A ...) (-> Any A ... A (List A ... A)))
#<procedure>

syntax
(λ formals . body)

An alias for the same form using lambda.

syntax
(case-lambda maybe-tvars [formals body] ...)

A function of multiple arities. The formals are identical to those accepted by the lambda form except that keyword and optional arguments are not allowed.

Polymorphic type variables, if provided, are bound in the type expressions in the formals.

Note that each formals must have a different arity.

Example:

> (define add-map
    (case-lambda
     [([lst : (Listof Integer)])
      (map add1 lst)]
     [([lst1 : (Listof Integer)]
       [lst2 : (Listof Integer)])
      (map + lst1 lst2)]))

To see how to declare a type for add-map, see the case-> type constructor.

2.3 Loops

syntax
(for type-ann-maybe (for:-clause ...)
expr ...+)

type-ann-maybe =
| : u

for-clause = [id : t seq-expr]
| [(binding ...) seq-expr]
| [id seq-expr]
| #:when guard

binding = id
| [id : t]

Like for from racket/base, but each id has the associated type t. Since the return type is always Void, annotating the return type of a for form is optional. Type annotations in clauses are optional for all for variants.

syntax
(for/list type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/hash type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/hasheq type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/hasheqv type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/vector type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/flvector type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/and type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/or type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/first type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/last type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/sum type-ann-maybe (for-clause ...) expr ...+)
syntax
(for/product type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/list type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/hash type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/hasheq type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/hasheqv type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/vector type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/flvector type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/and type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/or type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/first type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/last type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/sum type-ann-maybe (for-clause ...) expr ...+)
syntax
(for*/product type-ann-maybe (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 return value of the entire form must be of type u. For example, a for/list form would be annotated with a Listof type. All annotations are optional.

syntax
(for/lists type-ann-maybe ([id : t] ...)
  (for-clause ...)
  expr ...+)
syntax
(for/fold  type-ann-maybe ([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.

syntax
(for* void-ann-maybe (for-clause ...)
  expr ...+)
syntax
(for*/lists type-ann-maybe ([id : t] ...)
  (for-clause ...)
  expr ...+)
syntax
(for*/fold  type-ann-maybe ([id : t init-expr] ...)
  (for-clause ...)
  expr ...+)

These behave like their non-annotated counterparts.

syntax
(do : u ([id : t init-expr step-expr-maybe] ...)
(stop?-expr finish-expr ...)
expr ...+)

step-expr-maybe =
| step-expr

Like do from racket/base, but each id having the associated type t, and the final body expr having the type u. Type annotations are optional.

2.4 Definitions

syntax
(define maybe-tvars v maybe-ann e)
(define maybe-tvars header maybe-ann . body)

header = (function-name . formals)
| (header . formals)

formals = (formal ...)
| (formal ... . rst)

formal = var
| [var default-expr]
| [var : type]
| [var : type default-expr]
| keyword var
| keyword [var : type]
| keyword [var : type default-expr]

rst = var
| [var : type *]
| [var : type ooo bound]

maybe-tvars =
| #:forall (tvar ...)
| #:∀ (tvar ...)
| #:forall (tvar ... ooo)
| #:∀ (tvar ... ooo)

maybe-ann =
| : type

Like define from racket/base, but allows optional type annotations for the variables.

The first form defines a variable v to the result of evaluating the expression e. The variable may have an optional type annotation.

Examples:

> (define foo "foo")
> (define bar : Integer 10)

If polymorphic type variables are provided, then they are bound for use in the type annotation.

Example:

> (define #:forall (A) mt-seq : (Sequenceof A) empty-sequence)

The second form allows the definition of functions with optional type annotations on any variables. If a return type annotation is provided, it is used to check the result of the function.

Like lambda, optional and keyword arguments are supported.

Examples:

> (define (add [first : Integer]
               [rest  : Integer]) : Integer
    (+ first rest))
> (define #:forall (A)
          (poly-app [func : (A A -> A)]
                    [first : A]
                    [rest  : A]) : A
    (func first rest))

The function definition form also allows curried function arguments with corresponding type annotations.

Examples:

> (define ((addx [x : Number]) [y : Number]) (+ x y))
> (define add2 (addx 2))
> (add2 5)
- : Number
7

Note that unlike define from racket/base, define does not bind functions with keyword arguments to static information about those functions.

2.5 Structure Definitions

syntax
(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 from racket/base. 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. If parent is also a polymorphic struct, then there must be at least as many type variables as in the parent type, and the parent type is instantiated with a prefix of the type variables matching the amount it needs.

Options provided have the same meaning as for the struct form from racket/base.

syntax
(define-struct maybe-type-vars name-spec ([f : t] ...) options ...)

maybe-type-vars =
| (v ...)

name-spec = name
| (name parent)

options = #:transparent
| #:mutable

Legacy version of struct, corresponding to define-struct from racket/base.

syntax
(define-struct/exec name-spec ([f : t] ...) [e : proc-t])

name-spec = name
| (name parent)

Like define-struct, but defines a procedural structure. The procdure e is used as the value for prop:procedure, and must have type proc-t.

2.6 Names for Types

syntax
(define-type name t maybe-omit-def)
(define-type (name v ...) t maybe-omit-def)

maybe-omit-def = #:omit-define-syntaxes
|

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 or enclosing scopes.

Examples:

> (define-type IntStr (U Integer String))
> (define-type (ListofPairs A) (Listof (Pair A A)))

If #:omit-define-syntaxes is specified, no definition of name is created. In this case, some other definition of name is necessary.

If the body of the type definition refers to itself, then the type definition is recursive. Recursion may also occur mutually, if a type refers to a chain of other types that eventually refers back to itself.

Examples:

> (define-type BT (U Number (Pair BT BT)))
> (let ()
    (define-type (Even A) (U Null (Pairof A (Odd A))))
    (define-type (Odd A) (Pairof A (Even A)))
    (: even-lst (Even Integer))
    (define even-lst '(1 2))
    even-lst)
- : (Even Integer)
'(1 2)

However, the recursive reference may not occur immediately inside the type:

Examples:

> (define-type Foo Foo)
eval:34:0: Type Checker: Error in macro expansion --
Recursive types are not allowed directly inside their
definition
in: Foo
> (define-type Bar (U Bar False))
eval:35:0: Type Checker: Error in macro expansion --
Recursive types are not allowed directly inside their
definition
in: False

2.7 Generating Predicates Automatically

syntax
(make-predicate t)

Evaluates to a predicate for the type t, with the type (Any -> Boolean : t). t may not contain function types, or types that may refer to mutable data such as (Vectorof Integer).

syntax
(define-predicate name t)

Equivalent to (define name (make-predicate t)).

2.8 Type Annotation and Instantiation

syntax
(: v t)
(: v : t)

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.

Examples:

> (: var1 Integer)
> (: var2 String)

The second form allows type annotations to elide one level of parentheses for function types.

Examples:

> (: var3 : -> Integer)
> (: var4 : String -> Integer)

syntax
(provide: [v t] ...)

This declares that the vs have the types t, and also provides all of the vs.

syntax
#{v : t}

This declares that the variable v has type t. This is legal only for binding occurrences of v.

syntax
(ann e t)

Ensure that e has type t, or some subtype. The entire expression has type t. This is legal only in expression contexts.

syntax
#{e :: t}

A reader abbreviation for (ann e t).

syntax
(cast e t)

The entire expression has the type t, while e may have any type. The value of the entire expression is the value returned by e, protected by a contract ensuring that it has type t. This is legal only in expression contexts.

Examples:

> (cast 3 Integer)
- : Integer
3
> (cast 3 String)
- : String
3: broke its contract
  promised: String
  produced: 3
  in: String
  contract from: cast
  blaming: cast
  at: eval:41.0
> (cast (lambda: ([x : Any]) x) (String -> String))
- : (-> String String)
#<procedure:val>

syntax
(inst e t ...)
(inst e t ... t ooo bound)

Instantiate the type of e with types t ... or with the poly-dotted types t ... t ooo bound. e must have a polymorphic type that can be applied to the supplied number of type variables. This is legal only in expression contexts.

Examples:

> (foldl (inst cons Integer Integer) null (list 1 2 3 4))
- : (Listof Integer)
'(4 3 2 1)
> (: fold-list : (All (A) (Listof A) -> (Listof A)))
> (define (fold-list lst)
(foldl (inst cons A A) null lst))
> (fold-list (list "1" "2" "3" "4"))
- : (Listof String)
'("4" "3" "2" "1")
> (: my-values : (All (A B ...) (A B ... -> (values A B ... B))))
> (define (my-values arg . args)
(apply (inst values A B ... B) arg args))

syntax
#{e @ t ...}

A reader abbreviation for (inst e t ...).

syntax
#{e @ t ... t ooo bound}

A reader abbreviation for (inst e t ... t ooo bound).

2.9 Require

Here, m is a module spec, pred is an identifier naming a predicate, and maybe-renamed is an optionally-renamed identifier.

syntax
(require/typed m rt-clause ...)

rt-clause = [maybe-renamed t]
|
[#:struct name ([f : t] ...)
struct-option ...]
|
[#:struct (name parent) ([f : t] ...)
struct-option ...]
| [#:opaque t pred]

maybe-renamed = id
| (orig-id new-id)

struct-option = #:constructor-name constructor-id
| #:extra-constructor-name constructor-id

This form requires identifiers from the module m, giving them the specified types.

The first case requires maybe-renamed, giving it type t.

The second and third cases require the struct with name name with fields f ..., where each field has type t. The third case 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.

Examples:

> (module UNTYPED racket/base
    (define n 100)

    (struct IntTree
      (elem left right))

    (provide n (struct-out IntTree)))
> (module TYPED typed/racket
    (require/typed 'UNTYPED
                   [n Natural]
                   [#:struct IntTree
                     ([elem  : Integer]
                      [left  : IntTree]
                      [right : IntTree])]))

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.

Examples:

> (require/typed racket/base
                 [#:opaque Evt evt?]
                 [alarm-evt (Real -> Evt)]
                 [sync (Evt -> Any)])
eval:51:0: Type Checker: Type (-> Real Error) could not be
converted to a contract: contract generation not supported
for this type
  in: (Real -> Evt)
> evt?
eval:51:0: Type Checker: parse error in type;
type name `Evt' is unbound
  in: Evt
> (sync (alarm-evt (+ 100 (current-inexact-milliseconds))))
- : (Rec x (Evtof x))
#<alarm-evt>

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 the types of predicates such as number?, cannot be converted to contracts and raise a static error when used in a require/typed form. Here is an example of using case-> in require/typed.

(require/typed racket/base
               [file-or-directory-modify-seconds
                (case->
                  [String -> Exact-Nonnegative-Integer]
                  [String (Option Exact-Nonnegative-Integer)
                          ->
                          (U Exact-Nonnegative-Integer Void)]
                  [String (Option Exact-Nonnegative-Integer) (-> Any)
                          ->
                          Any])])

file-or-directory-modify-seconds has some arguments which are optional, so we need to use case->.

syntax
(require/typed/provide m rt-clause ...)

Similar to require/typed, but also provides the imported identifiers. Uses outside of a module top-level raise an error.

Examples:

> (module evts typed/racket
    (require/typed/provide racket/base
                           [#:opaque Evt evt?]
                           [alarm-evt (Real -> Evt)]
                           [sync (Evt -> Any)]))
> (require 'evts)
> (sync (alarm-evt (+ 100 (current-inexact-milliseconds))))
- : Any
#<alarm-evt>

2.10 Other Forms

syntax
with-handlers

Identical to with-handlers from racket/base but provides additional annotations to assist the typechecker.

procedure
(default-continuation-prompt-tag)
→ (-> (Prompt-Tagof Any (Any -> Any)))

Identical to default-continuation-prompt-tag, but additionally protects the resulting prompt tag with a contract that wraps higher-order values, such as functions, that are communicated with that prompt tag. If the wrapped value is used in untyped code, a contract error will be raised.

Examples:

> (module typed typed/racket
    (provide do-abort)
    (: do-abort (-> Void))
    (define (do-abort)
      (abort-current-continuation
       ; typed, and thus contracted, prompt tag
       (default-continuation-prompt-tag)
       (λ: ([x : Integer]) (+ 1 x)))))
> (module untyped racket
    (require 'typed)
    (call-with-continuation-prompt
      (λ () (do-abort))
      (default-continuation-prompt-tag)
      ; the function cannot be passed an argument
      (λ (f) (f 3))))
> (require 'untyped)
default-continuation-prompt-tag: broke its contract
  Attempted to use a higher-order value passed as `Any` in
untyped code: #<procedure>
  in: the range of
      (-> (prompt-tag/c Any #:call/cc Any))
  contract from: untyped
  blaming: untyped

syntax
(#%module-begin form ...)

Legal only in a module begin context. The #%module-begin form of typed/racket checks all the forms in the module, using the Typed Racket type checking rules. All provide forms are rewritten to insert contracts where appropriate. Otherwise, the #%module-begin form of typed/racket behaves like #%module-begin from racket.

syntax
(#%top-interaction . form)

Performs type checking of forms entered at the read-eval-print loop. The #%top-interaction form also prints the type of form after type checking.

top ← prev up next →

1	Type Reference
2	Special Form Reference
3	Libraries Provided With Typed Racket
4	Typed Classes
5	Utilities
6	Exploring Types
7	Typed Racket Syntax Without Type Checking
8	Typed Regions
9	Optimization in Typed Racket
10	Legacy Forms
11	Compatibility Languages
12	Experimental Features

2.1	Binding Forms
2.2	Anonymous Functions
2.3	Loops
2.4	Definitions
2.5	Structure Definitions
2.6	Names for Types
2.7	Generating Predicates Automatically
2.8	Type Annotation and Instantiation
2.9	Require
2.10	Other Forms