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
Listof could not be converted to a predicate: cannot
generate contract for non-function polymorphic type
in: (All (A) (Listof A))
8.4 Unsupported features
Most structure type properties do not work in Typed Racket, including support for 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—
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"
argument position: 2nd
other arguments...:
1
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"
argument position: 2nd
other arguments...:
1
> (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—
> (: 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