On this page:
with-type
8.11

10 Typed Regions

The with-type form allows for localized Typed Racket regions in otherwise untyped code.

syntax

(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

> ((with-type #:result (Number -> Number)
     (lambda: ([x : Number]) (add1 x)))
   #f)

.../contract/region.rkt:764:62: contract violation

  expected: number?

  given: #f

  in: the 1st argument of

      (-> number? any)

  contract from: (region typed-region)

  blaming: top-level

   (assuming the contract is correct)

> (let ([x "hello"])
    (with-type #:result String
      #:freevars ([x String])
      (string-append x ", world")))

"hello, world"

> (let ([x 'hello])
    (with-type #:result String
      #:freevars ([x String])
      (string-append x ", world")))

x: broke its own contract

  promised: string?

  produced: 'hello

  in: string?

  contract from: top-level

  blaming: top-level

   (assuming the contract is correct)

  at: eval:5:0

> (with-type ([fun (Number -> Number)]
              [val Number])
    (define (fun x) x)
    (define val 17))
> (fun val)

17