This section describes limitations and subtle aspects of the type system that programmers often stumble on while porting programs to Typed Racket.
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).
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)
The issue is that the type of cons is also polymorphic:
- : (All (a b) (case-> (-> a (Listof a) (Listof a)) (-> a b (Pairof a b))))
> (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))
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
String Bytes))) could not be converted to a contract:
function type has two cases of arity 1
in: (case-> (-> Struct-Type-Property Symbol) (-> Regexp (U
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 Symbol String Bytes)
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))
Most structure type properties do not work in Typed Racket, including support for generic interfaces.
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 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:
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
argument position: 2nd
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"))
+: contract violation
argument position: 2nd
eval:17:0: Type Checker: type mismatch
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.
Contract boundaries installed for typed-untyped interaction may cause significant slowdowns. See Contract boundaries for details.