6.11.0.2

## Hints on Using Typed Racket in CPE 430

John Clements <clements@calpoly.edu>

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.

Specifically, in Assignment 2, there two common situations you’re likely to encounter.

### 1Using Polymorphic Functions

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

(:print-type map)

... in the interactions window of a successfully-compiling TR program.

Here’s what I get:

 (All (c a b ...) (case-> (-> (-> a c) (Pairof a (Listof a)) (Pairof c (Listof c))) (-> (-> a b ... b c) (Listof a) (Listof b) ... b (Listof 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 All 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 (inst ...) form. Since we need to supply the types in the same order they’re specified in the All 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 (Listof (Listof 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) (Listof a) (Listof b) ... b -> (Listof c) (-> a c) (Pairof a (Listof a)) -> (Pairof c (Listof c)) Arguments: (All (a b) (case-> (-> (Pairof a (Listof b)) a) (-> (Listof a) a))) (Listof (Listof 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 inst:

 (: lon (Listof (Listof Number))) (define lon (list (list 3 4) (list 5) (list 6 7))) ((inst map Number (Listof Number)) first lon)

Alternatively, you can use inst to provide type parameters for first, instead, or you can even write a helper function that’s basically first with fixed types:

 (: firstlon ((Listof Number) -> Number)) (define firstlon first)

### 2Types for Lambda arguments

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))

### 3Casting/Asserting

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 cast or assert. So, for instance, if you know that s is a List of S-expressions, you can force a dynamic check like this:

(cast s (Listof 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 inst 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 (cast "banana" Real) 5)

Naturally, it will crash and burn at runtime.

#### 3.1Cast Justification

I’ve discovered that I can usually find lots of bugs in student programs by just jumping to their uses of cast; usually, every one of them is a latent bug. You should use cast 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 cast come with a one-line comment, indicating why this cast can’t fail. For instance:

 ;; sublist of Sexp must be (Listof Sexp)

### 4Boxes

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 inst. 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:

((inst 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.

### 5Hash Table Construction

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.