John Clements <email@example.com>
Typed Racket can do some very clever things, but there are cases in which it needs a little help in order to figure out what types to assign to various terms.
Here are a number of common situations you’re likely to encounter.
This error is caused by a failure to mark a structure as #:transparent. This prevents the test framework from inspecting its fields, and the type checker complains when the test framework tries to.
Another dead giveaway for this problem is any value that’s displayed with angle brackets, e.g.:
Just make sure to add #:transparent annotations to each of your structures, or use the tstruct macro that appears in the PLAI translation.
So, for instance, you might change
(struct NumC ([n Real]))
(struct NumC ([n Real]) #:transparent)
Functions like map are polymorphic. More specifically, in Typed Racket (henceforth ‘TR’), map has a type that uses what’s called ‘parametric polymorphism’. That is, the polymorphic type is parameterized by one or more input types.
If you want to see the type of map, in fact, you can simply run
... in the interactions window of a successfully-compiling TR program.
Here’s what I get:
( (c a b ...) (case-> ( ( a c) ( a ( a)) ( c ( c))) ( ( a b ... b c) ( a) ( b) ... b ( c))))
This type has all kinds of interesting things hiding in it; among them, the fact that map of a non-empty list is guaranteed to produce a non-empty list, and the fact that map can handle multiple input lists. Neither of those is relevant to us, here.
Most important is the fact that map is defined as an type, that is parameterized over 2 or 3 types. For us, we only care about the types c and a, the output and input types respectively for a single-list map.
When using map with TR, then, certain type errors arise because TR can’t figure out what types to use for a and c. One easy way to give TR a hint is to use the ( ...) form. Since we need to supply the types in the same order they’re specified in the form, we must provide the output type before the input type.
So, for instance, suppose we’re applying the first operation to a list of lists of numbers:
( lon ( ( Number))) (define lon (list (list 3 4) (list 5) (list 6 7))) (map first lon)
This will signal this error:
Type Checker: Polymorphic function `map'could not be applied to arguments: Types: ( a b ... b c) ( a) ( b) ... b ( c) ( a c) ( a ( a)) ( c ( c)) Arguments: ( (a b) (case-> ( ( a ( b)) a) ( ( a) a))) ( ( Number)) Expected result: AnyValues in: (map first lon)
The problem here is that there are too many free variables; both map and first are parameterized by type variables.
The solution is to provide the input and output types for map, using :
( lon ( ( Number))) (define lon (list (list 3 4) (list 5) (list 6 7))) (( map Number ( Number)) first lon)
Alternatively, you can use to provide type parameters for first, instead, or you can even write a helper function that’s basically first with fixed types:
( firstlon (( Number) Number)) (define firstlon first)
It’s often necessary to help TR out when defining an anonymous function using a lambda. So, for instance, if you write
(λ (arg) (subst sym (interp arg) body))
... TR may complain that arg has type Any. The solution here is usually to inform TR about the type of this argument, like this:
(λ ([arg ExprC]) (subst sym (interp arg) body))
There may be certain situations in which TR is unable to figure out that a certain value must have a certain type. In cases like this, it may be useful to insert a dynamic check using or assert. So, for instance, if you know that s is a List of S-expressions, you can force a dynamic check like this:
( s ( Sexp))
Note that this is (a) a bit of an “I give up” move, and (b) somewhat dangerous, because this check can fail at runtime. As a rule, you’d like to be able to convince TR that the thing has the type without requiring a dynamic cast. Still, especially in the presence of match, this may not always be possible.
Note that a cast is very different from a simple annotation, like the or the types for lambda arguments, because it actually inserts a dynamic check. Rather than trying to nudge TR toward seeing that the code type-checks, you’re simply inserting a dynamic check to force it to that type.
To give an extreme example, this code type-checks just fine:
(+ 3 4 ( "banana" Real) 5)
Naturally, it will crash and burn at runtime.
I’ve discovered that I can usually find lots of bugs in student programs by just jumping to their uses of ; usually, every one of them is a latent bug. You should use only when you’ve already checked (or match has already checked) that the cast will succeed.
To address this, I’m now requiring that every use of come with a one-line comment, indicating why this cast can’t fail. For instance:
;; sublist of Sexp must be (Listof Sexp)
We don’t come across mutable boxes until fairly late in the class, but they present a particular problem for a system such as Typed Racket that attempts to infer types.
Here’s the problem. For an ordinary term such as 3 or 'rabbit, it’s fine to assign it a more specific type than the context requires. For instance, if you have a function that accepts a real, and you pass it an integer, that’s fine, because integers are a subtype of reals.
However, for mutable boxes, things break. That’s because (Boxof Integer) is not a subtype of (Boxof Real). To see this, suppose your function accepts a (Boxof Real), and I pass it a (Boxof Integer). Now, suppose your function puts the value 3.6 in the box (should be okay, it’s a box of Reals as far as your function is concerned. Now, the function ends, and my code continues running. But wait! My (Boxof Integer) now contains the value 3.6!
For this reason, Typed Racket can’t simply guess a more precise type for a box, because if it guesses wrong, the value will be unusable. In this case, then, it’s nearly always necessary to explicitly annotate a box with it’s expected type, using an . So, for instance, if in your program NumV is a subtype of Value, and you want to create a Boxof Value containing a (NumV 6), you’ll have to write:
(( box Value) (NumV 6))
It’s worth noting that Java and other languages have this probelem, too; it’s hard to do a good job of inferring types for mutable variables.
There are a variety of ways to construct hash tables. Many of them will cause you some grief.
The first way is to use hash literals. For instance:
#hash((3 . 4) (5 . 6) (a . 123) (z . f) (hth . 23412))
This works fine, but you need to know that this form is like a quote; it puts the reader in "quote" mode, so that the a, z, and f are not variable references, but rather symbols. If you write code like this:
(define (f [x Real]) (+ x 23)) #hash((3 . 4) (5 . 6) (a . (+ 12 13)) (z . f) (hth . 23412))
... you might be dismayed to see that the key 'z is bound not to the function f, but rather to the symbol 'f. Also, the key 'a is bound to a list containing symbols and numbers, rather than to the number 25.
You may also be dismayed to see those periods in there. It turns out that this is the literal syntax for cons pairs; I haven’t bothered to show it to you before, because we haven’t needed it.
You can also create hashes using simply hash. The problem with hash is that it’s a variable arity function, and TR has special-case types for up to some fixed number of arguments. Could be six. If you go beyond this limit, you’ll see that TR just gives up.
Here’s the TL/DR:
The final and most bulletproof way to construct a hash is to use make-immutable-hash, which takes a list of pairs and returns a hash table:
(define (f [x Real]) (+ x 23)) (make-immutable-hash (list (cons 3 4) (cons 5 6) (cons 'a 123) (cons 'z f) (cons 'hth 23412)))
Running this example shows that the symbol 'z is bound now to the function f, as desired.