6 Typed-Untyped Interaction

In the previous sections, all of the examples have consisted of programs that are entirely typed. One of the key features of Typed Racket is that it allows the combination of both typed and untyped code in a single program.

6.1 Using Untyped Code from Typed Code

Suppose that we write the untyped module from Quick Start again:

"distance.rkt"

#lang racket

(provide (struct-out pt)

distance)

(struct pt (x y))

; distance : pt pt -> real

(define (distance p1 p2)

(sqrt (+ (sqr (- (pt-x p2) (pt-x p1)))

(sqr (- (pt-y p2) (pt-y p1))))))

If we want to use the distance function defined in the above module from a typed module, we need to use the require/typed form to import it. Since the untyped module did not specify any types, we need to annotate the imports with types (just like how the example in Quick Start had additional type annotations with :):

Note that a typed module does not need to use require/typed to import from another typed module. The require form will work in such cases.

"client.rkt"

#lang typed/racket

(require/typed "distance.rkt"

[#:struct pt ([x : Real] [y : Real])]

[distance (-> pt pt Real)])

(distance (pt 3 5) (pt 7 0))

The require/typed form has several kinds of clauses. The #:struct clause specifies the import of a structure type and allows us to use the structure type as if it were defined with Typed Racket’s struct.

The second clause in the example above specifies that a given binding distance has the given type (-> pt pt Real).

Note that the require/typed form can import bindings from any module, including those that are part of the Racket standard library. For example,

#lang typed/racket

(require/typed racket/base [add1 (-> Integer Integer)])

is a valid use of the require/typed form and imports add1 from the racket/base library.

6.1.1 Opaque Types

The #:opaque clause of require/typed defines a new type using a predicate from untyped code. Suppose we have an untyped distance function that uses pairs of numbers as points:

"distance2.rkt"

#lang racket

(provide point?

distance)

; A Point is a (cons real real)

(define (point? x)

(and (pair? x)

(real? (car x))

(real? (cdr x))))

; distance : Point Point -> real

(define (distance p1 p2)

(sqrt (+ (sqr (- (car p2) (car p1)))

(sqr (- (cdr p2) (cdr p1))))))

A typed module can use #:opaque to define a Point type as all values that the point? predicate returns #t for:

"client2.rkt"

#lang typed/racket

(require/typed "distance2.rkt"

[#:opaque Point point?]

[distance (-> Point Point Real)])

(define p0 : Point (assert (cons 3 5) point?))

(define p1 : Point (assert (cons 7 0) point?))

(distance p0 p1)

6.2 Using Typed Code in Untyped Code

In the previous subsection, we saw that the use of untyped code from typed code requires the use of require/typed. However, the use of code in the other direction (i.e., the use of typed code from untyped code) requires no additional work.

If an untyped module requires a typed module, it will be able to use the bindings defined in the typed module as expected. The major exception to this rule is that macros defined in typed modules may not be used in untyped modules.

6.3 Protecting Typed-Untyped Interaction

One might wonder if the interactions described in the first two subsections are actually safe; after all, untyped code might be able to ignore the errors that Typed Racket’s type system will catch at compile-time.

To ensure that typed-untyped interactions are safe, Typed Racket establishes contracts wherever typed and untyped code interact. For example, suppose that we write an untyped module that implements an increment function:

For general information on Racket’s contract system , see Contracts.

> (module increment racket     (provide increment)        ; increment : exact-integer? -> exact-integer?     (define (increment x) "this is broken"))

and a typed module that uses it:

> (module client typed/racket        (require/typed 'increment [increment (-> Integer Integer)])        (increment 5))

This combined program is not correct. All uses of increment in Typed Racket are correct under the assumption that the increment function upholds the (-> Integer Integer) type. Unfortunately, our increment implementation does not actually uphold this assumption, because the function actually produces strings.

On the other hand, when the program is run:

> (require 'client)

increment: broke its own contract

promised: exact-integer?

produced: "this is broken"

in: (-> any/c exact-integer?)

contract from: (interface for increment)

blaming: (interface for increment)

(assuming the contract is correct)

at: eval:3.0

we find that the contract system checks the assumption made by the typed module and correctly finds that the assumption failed because of the implementation in the untyped module (hence it is blamed in the error message).

In the same fashion, Typed Racket checks all functions and other values that pass from a typed module to untyped module or vice versa with contracts. This means that, for example, Typed Racket can safely optimize programs (see Optimization in Typed Racket) with the assurance that the program will not segfault due to an unchecked assumption.

Important caveat: contracts such as the Integer check from above are performant. However, contracts in general can have a non-trivial performance impact, especially with the use of first-class functions or other higher-order data such as vectors.

Note that no contract overhead is ever incurred for uses of typed values from another typed module.