Hints on Using Typed Racket in CPE 430
1 Don’t Use Type ‘Number’
2 Don’t use predicate ‘integer?‘
3 Unable to protect opaque value passed as ‘Any‘
4 Using Polymorphic Functions
5 Types for Lambda arguments
6 Predicate Patterns with Dot-dot-dot
7 Other Casting
8 Cast vs. Inst vs. Annotation
9 Boxes
10 Hash Table Construction
7.5.0.6

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

2 Don’t use predicate ‘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.

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

#<NumC>

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)

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

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

6 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.

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

8 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.

9 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. 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.

10 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.

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.