On this page:
with-type
Version: 5.1.3

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

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

contract violation: expected <Number>, given: #f

  contract from (region typed-region), blaming top-level

  contract: (-> Number Number)

> (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: self-contract violation, expected <String>, given: 'hello

  contract from top-level, blaming top-level

  contract: String

        at: eval:5.0

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

17