▼The Typed Racket Reference
►6 Utilities
On this page:
assert
with-asserts
defined?
index?
typecheck-fail
assert-typecheck-fail
6.1 Ignoring type information
6.2 Untyped Utilities
require/  untyped-contract
define-typed/  untyped-identifier
syntax-local-typed-context?
8.5
  top  contents  ← prev  up  next → 

6 Utilities

Typed Racket provides some additional utility functions to facilitate typed programming.

procedure

(assert v) → A

  v : (U #f A)
(assert v p?) → B
  v : A
  p? : (A -> Any : B)
Verifies that the argument satisfies the constraint. If no predicate is provided, simply checks that the value is not #f.

See also the cast form.

Examples:
> (define: x : (U #f String) (number->string 7))
> x

- : (U False String)

"7"

> (assert x)

- : String

"7"

> (define: y : (U String Symbol) "hello")
> y

- : (U String Symbol)

"hello"

> (assert y string?)

- : String

"hello"

> (assert y boolean?)

Assertion #<procedure:boolean?> failed on "hello"

syntax

(with-asserts ([id maybe-pred] ...) body ...+)

 
maybe-pred = 
  | predicate
Guard the body with assertions. If any of the assertions fail, the program errors. These assertions behave like assert.

procedure

(defined? v) → boolean?

  v : any/c
A predicate for determining if v is not #<undefined>.

procedure

(index? v) → boolean?

  v : any/c
A predicate for the Index type.

syntax

(typecheck-fail orig-stx maybe-msg maybe-id)

 
maybe-msg = 
  | msg-string
     
maybe-id = 
  | #:covered-id id
Explicitly produce a type error, with the source location or orig-stx. If msg-string is present, it must be a literal string, it is used as the error message, otherwise the error message "Incomplete case coverage" is used. If id is present and has type T, then the message "missing coverage of T" is added to the error message.

Examples:
> (define-syntax (cond* stx)
    (syntax-case stx ()
      [(_ x clause ...)
       #`(cond clause ... [else (typecheck-fail #,stx "incomplete coverage"
                                                #:covered-id x)])]))
> (define: (f [x  : (U String Integer)]) : Boolean
    (cond* x
           [(string? x) #t]
           [(exact-nonnegative-integer? x) #f]))

eval:10:0: Type Checker: incomplete coverage; missing

coverage of Negative-Integer

  in: #f

syntax

(assert-typecheck-fail body-expr)

(assert-typecheck-fail body-expr #:result result-expr)
Explicitly produce a type error if body-expr does not produce a type error. If result-expr is provided, it will be the result of evaluating the expression, otherwise (void) will be returned. If there is an expected type, that type is propagated as the expected type when checking body-expr.

Added in version 1.7 of package typed-racket-lib.

6.1 Ignoring type information

In some contexts, it is useful to have the typechecker forget type information on particular expressions. Any expression with the shape (#%expression sub) that has a true value for the syntax property 'typed-racket:ignore-type-information will have the type Any, and the type checker won’t learn anything about the expression for use in refining other types.

Added in version 1.7 of package typed-racket-lib.

The expression sub must still type check, but can have any single-valued type.

This is similar to (ann sub Any), but differs in whether the typechecker can use this to refine other types, and can be used in context that do not depend on Typed Racket.

6.2 Untyped Utilities

 (require typed/untyped-utils) package: typed-racket-lib

These utilities help interface typed with untyped code, particularly typed libraries that use types that cannot be converted into contracts, or export syntax transformers that must expand differently in typed and untyped contexts.

Changed in version 1.14 of package typed-racket-lib: The module moved from typed-racket-more to typed-racket-lib.

syntax

(require/untyped-contract maybe-begin module [name subtype] ...)

 
maybe-begin = 
  | (begin expr ...)
Use this form to import typed identifiers whose types cannot be converted into contracts, but have subtypes that can be converted into contracts.

For example, suppose we define and provide the Typed Racket function
(: negate (case-> (-> Index Fixnum)
                  (-> Integer Integer)))
(define (negate x) (- x))
Trying to use negate within an untyped module will raise an error because the cases cannot be distinguished by arity alone.

If the defining module for negate is "my-numerics.rkt", it can be imported and used in untyped code this way:
(require/untyped-contract
 "my-numerics.rkt"
 [negate  (-> Integer Integer)])
The type (-> Integer Integer) is converted into the contract used for negate.

The require/untyped-contract form expands into a submodule with language typed/racket/base. Identifiers used in subtype expressions must be either in Typed Racket’s base type environment (e.g. Integer and Listof) or defined by an expression in the maybe-begin form, which is spliced into the submodule. For example, the math/matrix module imports and reexports matrix-expt, which has a case-> type, for untyped use in this way:
(provide matrix-expt)
 
(require/untyped-contract
 (begin (require "private/matrix/matrix-types.rkt"))
 "private/matrix/matrix-expt.rkt"
 [matrix-expt  ((Matrix Number) Integer -> (Matrix Number))])
The (require "private/matrix/matrix-types.rkt") expression imports the Matrix type.

If an identifier name is imported using require/untyped-contract, reexported, and imported into typed code, it has its original type, not subtype. In other words, subtype is used only to generate a contract for name, not to narrow its type.

Because of limitations in the macro expander, require/untyped-contract cannot currently be used in typed code.

syntax

(define-typed/untyped-identifier name typed-name untyped-name)

Defines an identifier name that expands to typed-name in typed contexts and to untyped-name in untyped contexts. Each subform must be an identifier.

Suppose we define and provide a Typed Racket function with this type:

(: my-filter (All (a) (-> (-> Any Any : a) (Listof Any) (Listof a))))

This type cannot be converted into a contract because it accepts a predicate. Worse, require/untyped-contract does not help because (All (a) (-> (-> Any Any) (Listof Any) (Listof a))) is not a subtype.

In this case, we might still provide my-filter to untyped code using
(provide my-filter)
 
(define-typed/untyped-identifier my-filter
  typed:my-filter
  untyped:my-filter)
where typed:my-filter is the original my-filter, but imported using prefix-in, and untyped:my-filter is either a Typed Racket implementation of it with type (All (a) (-> (-> Any Any) (Listof Any) (Listof a))) or an untyped Racket implementation.

Avoid this if possible. Use only in cases where a type has no subtype that can be converted to a contract; i.e. cases in which require/untyped-contract cannot be used.

procedure

(syntax-local-typed-context?) → boolean?

Returns #t if called while expanding code in a typed context; otherwise #f.

This is the nuclear option, provided because it is sometimes, but rarely, useful. Avoid.

  top  contents  ← prev  up  next →