8 Caveats and Limitations🔗ℹ

This section describes limitations and subtle aspects of the type system that programmers often stumble on while porting programs to Typed Racket.

8.1 The Integer type and integer?🔗ℹ

In Typed Racket, the Integer type corresponds to values that return #t for the exact-integer? predicate, not the integer? predicate. In particular, values that return #t for integer? may be inexact numbers (e.g, 1.0).

When porting a program to Typed Racket, you may need to replace uses of functions like round and floor with corresponding exact functions like exact-round and exact-floor.

In other cases, it may be necessary to use assertions or casts.

8.2 Type inference for polymorphic functions🔗ℹ

Typed Racket’s local type inference algorithm is currently not able to infer types for polymorphic functions that are used on higher-order arguments that are themselves polymorphic.

For example, the following program results in a type error that demonstrates this limitation:

> (map cons '(a b c d) '(1 2 3 4))

eval:2:0: Type Checker: Polymorphic function `map' could not

be applied to arguments:

Domains: (-> a b ... b c) (Listof a) (Listof b) ... b

(-> a c) (Pairof a (Listof a))

Arguments: (All (a b) (case-> (-> a (Listof a) (Listof a))

(-> a b (Pairof a b)))) (List 'a 'b 'c 'd) (List One

Positive-Byte Positive-Byte Positive-Byte)

in: 4

The issue is that the type of cons is also polymorphic:

> cons

- : (All (a b) (case-> (-> a (Listof a) (Listof a)) (-> a b (Pairof a b))))

#<procedure:cons>

To make this expression type-check, the inst form can be used to instantiate the polymorphic argument (e.g., cons) at a specific type:

> (map (inst cons Symbol Integer) '(a b c d) '(1 2 3 4))

- : (Listof (Pairof Symbol Integer))

'((a . 1) (b . 2) (c . 3) (d . 4))

8.3 Typed-untyped interaction and contract generation🔗ℹ

When a typed module requires bindings from an untyped module (or vice-versa), there are some types that cannot be converted to a corresponding contract.

This could happen because a type is not yet supported in the contract system, because Typed Racket’s contract generator has not been updated, or because the contract is too difficult to generate. In some of these cases, the limitation will be fixed in a future release.

The following illustrates an example type that cannot be converted to a contract:

> (require/typed racket/base     [object-name (case-> (-> Struct-Type-Property Symbol)                          (-> Regexp (U String Bytes)))])

eval:5:0: Type Checker: Error in macro expansion -- Type

(case-> (-> Struct-Type-Property Symbol) (-> Regexp (U Bytes

String))) could not be converted to a contract: function

type has two cases of arity 1

in: (case-> (-> Struct-Type-Property Symbol) (-> Regexp (U

String Bytes)))

This function type by cases is a valid type, but a corresponding contract is difficult to generate because the check on the result depends on the check on the domain. In the future, this may be supported with dependent contracts.

A more approximate type will work for this case, but with a loss of type precision at use sites:

> (require/typed racket/base     [object-name (-> (U Struct-Type-Property Regexp)                      (U String Bytes Symbol))])

> (object-name #rx"a regexp")

- : (U Bytes String Symbol)

"a regexp"

Use of define-predicate also involves contract generation, and so some types cannot have predicates generated for them. The following illustrates a type for which a predicate can’t be generated:

> (define-predicate p? (All (A) (Listof A)))

eval:8:0: Type Checker: Error in macro expansion -- Type

(All (A) (Listof A)) could not be converted to a predicate:

cannot generate contract for non-function polymorphic type

in: (All (A) (Listof A))

8.4 Unsupported features🔗ℹ

Typed Racket currently does not support generic interfaces.

8.5 Type generalization🔗ℹ

Not so much a caveat as a feature that may have unexpected consequences. To make programming with invariant type constructors (such as Boxof) easier, Typed Racket generalizes types that are used as arguments to invariant type constructors. For example:

> 0

- : Integer [more precisely: Zero]

0

> (define b (box 0))

> b

- : (Boxof Integer)

'#&0

0 has type Zero, which means that b “should” have type (Boxof Zero). On the other hand, that type is not especially useful, as it only allows 0 to be stored in the box. Most likely, the intent was to have a box of a more general type (such as Integer) and initialize it with 0. Type generalization does exactly that.

In some cases, however, type generalization can lead to unexpected results:

> (box (ann 1 Fixnum))

- : (Boxof Integer)

'#&1

The intent of this code may be to create of box of Fixnum, but Typed Racket will generalize it anyway. To create a box of Fixnum, the box itself should have a type annotation:

> (ann (box 1) (Boxof Fixnum))

- : (Boxof Fixnum)

'#&1

> ((inst box Fixnum) 1)

- : (Boxof Fixnum)

'#&1

8.6 Macros and compile-time computation🔗ℹ

Typed Racket will type-check all expressions at the run-time phase of the given module and will prevent errors that would occur at run-time. However, expressions at compile-time—including computations that occur inside macros—are not checked.

Concretely, this means that expressions inside, for example, a begin-for-syntax block are not checked:

> (begin-for-syntax (+ 1 "foo"))

+: contract violation

expected: number?

given: "foo"

Similarly, expressions inside of macros defined in Typed Racket are not type-checked. On the other hand, the macro’s expansion is always type-checked:

(define-syntax (example-1 stx)   (+ 1 "foo")   #'1)

(define-syntax (example-2 stx)   #'(+ 1 "foo"))

> (example-1)

+: contract violation

expected: number?

given: "foo"

> (example-2)

eval:17:0: Type Checker: type mismatch

expected: Number

given: String

in: (quote "foo")

Note that functions defined in Typed Racket that are used at compile-time in other typed modules or untyped modules will be type-checked and then protected with contracts as described in Typed-Untyped Interaction.

Additionally, macros that are defined in Typed Racket modules cannot be used in ordinary Racket modules because such uses can circumvent the protections of the type system.

8.7 Expensive contract boundaries🔗ℹ

Contract boundaries installed for typed-untyped interaction may cause significant slowdowns. See Contract boundaries for details.

8.8 Pattern Matching and Occurrence Typing🔗ℹ

Because Typed Racket type checks code after macro expansion, certain forms—such as match—are difficult for Typed Racket to reason about completely. In particular, in a match clause, the type of an identifier is often not updated to reflect the fact that a previous pattern failed to match. For example, in the following function, the type checker is unaware that if execution reaches the last clause then the string? predicate has already failed to match on the value for x, and so (abs x) in the last clause fails to type check:

> (: size (-> (U String Integer) Integer))

> (define (size x)     (match x       [(? string?) (string-length x)]       [_ (abs x)]))

eval:21:0: Type Checker: type mismatch

expected: Integer

given: (U Integer String)

in: x

Because they are much simpler forms, similar cond and if expressions do type check successfully:

> (: size (-> (U String Integer) Integer))

> (define (size x)       (cond         [(string? x) (string-length x)]         [else (abs x)]))

One work around is to simply not rely on a catch-all "else" clause that needs to know that previous patterns have failed to match in order to type check:

> (: size (-> (U String Integer) Integer))

> (define (size x)       (match x         [(? string?) (string-length x)]         [(? exact-integer?) (abs x)]))

It is important to note, however, that match always inserts a catch-all failure clause if one is not provided! This means that the type checker will not inform the programmer that match clause coverage is insufficient because the implicit (i.e. macro-inserted) failure clause will cover any cases the programmer failed to anticipate with their pattern matching, e.g.:

> (: size (-> (U String Integer) Integer))

> (define (size x)       (match x         [(? string?) (string-length x)]))

> (size 42)

match: no matching clause for 42

Patterns involving an ellipsis ... for repetition may generate a for loop that requires annotations on variables to type check. The (deliberately obscure) code below does not type check without the type annotation on the match pattern variable c.

(: do-nothing (-> (Listof Integer) (Listof Integer)))

(define (do-nothing lst)

(match lst

[(list (? number? #{c : (Listof Integer)}) ...)   c]))

8.9 is-a? and Occurrence Typing🔗ℹ

Typed Racket does not use the is-a? predicate to refine object types because the target object may have been created in untyped code and is-a? does not check the types of fields and methods.

For example, the code below defines a class type Pizza%, a subclass type Sauce-Pizza%, and a function get-sauce (this function contains a type error). The get-sauce function uses is-a? to test the class of its argument; if the test is successful, the function expects the argument to have a field named topping that contains a value of type Sauce.

#lang typed/racket

(define-type Pizza%

(Class (field [topping Any])))

(define-type Sauce

(U 'tomato 'bbq 'no-sauce))

(define-type Sauce-Pizza%

(Class #:implements Pizza% (field [topping Sauce])))

(define sauce-pizza% : Sauce-Pizza%

(class object%

(super-new)

(field [topping 'tomato])))

(define (get-sauce [pizza : (Instance Pizza%)]) : Sauce

(cond

[(is-a? pizza sauce-pizza%)

(get-field topping pizza)] ; type error

[else

'bbq]))

The type-error message explains that (get-field topping pizza) can return any kind of value, even when pizza is an instance of the sauce-pizza% class. In particular, pizza could be an instance of an untyped subclass that sets its topping to the integer 0:

; #lang racket

(define evil-pizza%

(class sauce-pizza%

(inherit-field topping)

(super-new)

(set! topping 0)))

To downcast as intended, add a cast after the is-a? test. Below is a complete example that passes the type checker and raises a run-time error to prevent the typed get-sauce function from returning a non-Sauce value.