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.

Here are a number of common situations you’re likely to encounter.

1 Every ‘cond’ needs an ‘else’

For historical reasons, Racket’s cond behaves differently from match, in a way that can cause problems. Specifically, a cond where every clause’s test returns #f simply evaluates to (void), rather than signaling an error as match does.

Unfortunately, this means that the type-checker in typed racket has to consider the possibility that all clauses fail, unless there happens to be an else clause, because these are guaranteed to match.

This means that in the vast majority of cases, any cond that doesn’t have an else clause will be assumed to be able to return (void).

Solution? Either add an else clause that signals an error, or (if the last clause is guaranteed to suceed) simply replace the last test expression with else.

2 Don’t Use Type ‘Number’

You might be surprised to discover that typed racket’s Number type includes complex numbers. I have no plans to use any complex numbers in this course, as delightful as they are, so you probably want to use the Real type instead of the Number type across the board.

3 Don’t use predicate ‘integer?‘ or ‘nonnegative-integer?‘

want to check whether something is an integer? Use the exact-integer? predicate, not the integer? predicate. The problem is that integer? also returns #t for inexact numbers like 3.0, which means that a value v may pass a (integer? v) check but then fail to have the type Integer.

The same goes for nonnegative-integer?, use instead exact-nonnegative-integer?.

4 Unable to protect opaque value passed as ‘Any‘

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

into

(struct NumC ([n : Real]) #:transparent)

5 Using 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 real numbers:

(: lon (Listof (Listof Real)))

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

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

(define lon (list (list 3 4) (list 5) (list 6 7)))

((inst map Real (Listof Real)) 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 Real) -> Real))

(define firstlon first)

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

Please don’t use a cast for this.

7 Predicate Patterns with Dot-dot-dot

The compilation process for match is complicated, and can give TR a hard job.

Specifically, when we have a pattern variable that uses a question-mark pattern followed by dots, TR is unable to conclude that the variable has the type implied by the test.

Here’s an example that doesn’t work:

#lang typed/racket

(define (my-fun [s : Sexp]) : (Listof Symbol)

(match s

[(list 'x1 (? symbol? rst) ...)

;; TR can't conclude that rst has the type (Listof Symbol):

rst]

[(list (? symbol? fst) (? symbol? rst) ...)

(list fst)]))

Mousing over things to see types will only work if background expansion is turned on.... Mousing over the rst in the "answer" part of the first match clause shows that TR is giving it the type (Listof Any), even though the predicate guarantees that it must be a list of symbols. Note that there’s no similar problem with fst; if you mouse over it, you’ll see that it is given type Symbol.

To fix this, you need a cast, which inserts a runtime check. Like this:

#lang typed/racket

(define (my-fun [s : Sexp]) : (Listof Symbol)

(match s

[(list 'x1 (? symbol? rst) ...)

;; cast must succeed by definition of pattern above

(cast rst (Listof Symbol))]

[(list (? symbol? fst) (? symbol? rst) ...)

(list fst)]))

Now, the program type-checks.

8 Other Casting

Nearly every use of cast that is not occasioned by the kind of match problem mentioned in the previous problem turns out to be a bug in your code. This is because these casts are typically necessary because TR is correctly deducing that your value may not have the type that it expects, and adding a cast is just a way of telling TR to get stuffed. If TR is right, though, then this will turn out to be a cast that can fail, which will be an error in your code.

So: I will search for uses of cast in your code, and use them to try to break your program. You have been warned! (smiley....)

9 Computing a value twice

One of the more common reasons for a cast is that you are computing a value twice. Consider the following code:

(define (interp [e : ExprC] [env : Env]) : Value

(match e

[(IfC test then els)

(cond [(BoolV? (interp test env))

(cond [(BoolV-b (interp test env)) (interp els env)]

[else (interp then env)])]

[else (error 'interp "If test was not a boolean in expression: ~e" e)])]

[other (error 'interp "all other forms unimplemented... :(")]))

Typed Racket will signal an error here when you call BoolV-b on the result of (interp test env). "That’s silly," you might say, "I know that it must be a boolean, because I just checked on the line above with the BoolV? test!" The problem here is that you’re calling interp *again*, and Typed Racket reasonably concludes that just because it returned a BoolV the first time doesn’t mean that it will necessarily return a BoolV the second time. The solution is to give a name to the value, so that Typed Racket can see that it must be the same value:

(define (interp [e : ExprC] [env : Env]) : Value

(match e

[(IfC test then els)

(define test-result (interp test env))

(cond [(BoolV? test-result)

(cond [(BoolV-b test-result) (interp els env)]

[else (interp then env)])]

[else (error 'interp "If test was not a boolean in expression: ~e" e)])]

[other (error 'interp "all other forms unimplemented... :(")]))

This code does not have the type error for the call of BoolV-b on test-result.

There might be another bug in this code, though, you probably shouldn’t just copy it....

10 Cast vs. Inst vs. Annotation

Note that a cast is very different from a simple annotation, like the inst or the types for lambda arguments or the ann form, because cast simply assumes that you’re right at compile-time, and 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.

Compare this to the following:

(+ 3 4 (ann "banana" Real) 5)

This signals the error

... as you’d expect. The difference is that the ann form is making a *suggestion* to Typed Racket: "hey! Maybe *this* is the right type to use for this term." When you use a cast, by contrast, you’re saying "Perform this check at runtime, and for now just assume that it will succeed."

11 Boxes

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. However, you can do this just once, and give it a name. So, for instance, if your program includes

(define boxi (inst box Integer))

... then you could create a bunch of integer boxes like this:

(list (boxi 34) (boxi -342) (boxi 0))

Note that in your case, Integer probably isn’t the type you want!

It’s worth noting that Java and other languages have this problem, too; it’s hard to do a good job of inferring types for mutable variables.

12 Immutable Hash 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.

Instead, it’s best to create hashes with make-immutable-hash or just hash. These are similar, but the first one accepts a list of cons pairs, and the second one is a variable-arity function that pairs up its arguments to build the table.

These two examples both produce the same tree:

(define (f [x : Real]) (+ x 23))

;; using make-immutable-hash:

(make-immutable-hash

(list (cons 3 4)

(cons 5 6)

(cons 'a 123)

(cons 'z f)

(cons 'hth 23412)))

;; using hash:

(hash 3 4

5 6

'a 123

'z f

'hth 23412)

The second one is shorter, but if you want to do something interesting like passing in the list after constructing it separately, the first one is probably a bit more straightforward. It’s up to you.

Running either of these examples shows that the symbol 'z is bound now to the function f, as desired.

13 Mutable Hash Table Construction

It turns out that constructing a mutable hash table also has some issues.

Here’s the number one rule of mutable hash tables:

Don’t use cast on mutable hash tables!

The problem here is that this cast inserts a dynamic check but doesn’t change the contract associated with the underlying hash table, so you can wind up getting some very weird dynamic errors.

Instead, you probably want to supply a type when you create the hash table, using the ann annotation form.

So, for instance, let’s say I wanted to create a mutable hash table mapping strings to Integers, including initial bindings from 'a to 7 and 'b to 5. Here’s how I’d write that:

(define-type MyTable (Mutable-HashTable Symbol Integer))

(define my-table

(ann (make-hash

(list (cons 'a 5)

(cons 'b 7)))

MyTable))

(hash-set! my-table 'c 1000)