Typed Racket v7.0 Prefab Changes/Fixes

Typed Racket v7.0 Prefab Changes

For some time now, Typed Racket has unsoundly type checked prefab structs. This bug been fixed for the Racket v7.0 release (for more info, see the relevant Typed Racket RFC and the illustrative examples in the Prefab section of the docs). If you suspect your prefab-utilizing Typed Racket code no longer type checks because of this fix, we hope the below instructions help make any necessary changes as painless as possible. We apologize for any inconvenience. If you believe there are issues/fixes that should be added to this list, please do let us know.

(1) Why doesn't my prefab predicate work?

Consider the following prefab struct definition:

(struct point ([x : Number] [y : Number]) #:prefab)

Previously (Racket versions prior to 7.0) the following would type check:

(: sum-point (-> Any Number))
(define (sum-point p)
  (cond
    [(point? p)
      (+ (point-x p) (point-y p))]
    [else (error "not a point! ~a" p)]))

However, in Racket 7.0 and beyond, Typed Racket will complain with the following error messages:

Type Checker: type mismatch
  expected: Number
  given: Any in: (point-x p)

Type Checker: type mismatch
  expected: Number
  given: Any in: (point-y p)

This is because point? only tests if the value is a prefab structure with key 'point and has 2 fields and says nothing about the contents of the fields. In other words, point? is a predicate for the type (Prefab point Any Any) (if the prefab is immutable). If point were a mutable prefab struct, the predicate would be for the type (PrefabTop point 2), which is a type for a prefab that can be read from, but not written to (since we do now know what type to enforce for the mutable fields).

Fixes for this could involve any of the following:

Manually Inspecting Field Values

Manually testing the values produced by (point-x p) and (point-y p) with number? is one (perhaps verbose) way to fix the issue.

You can test the fields directly:

(: sum-point (-> Any Number))
(define (sum-point p)
  (cond
    [(and (point? p)
          (number? (point-x p))
          (number? (point-y p)))
      (+ (point-x p) (point-y p))]
    [else (error "not a valid point! ~a" p)]))

Or you can let bind them and then test them:

(: sum-point (-> Any Number))
(define (sum-point p)
  (cond
    [(point? p)
     (let ([x (point-x p)]
           [y (point-x p)])
       (if (and (number? x)
                (number? y))
           (+ x y)
           (error "not a valid point! ~a" p)))]
    [else (error "not a valid point! ~a" p)]))

Defining a predicate automatically

You can define a predicate for the type which includes the field types (as long as the field types are 1st order):

(define-predicate valid-point? point)

(: sum-point (-> Any Number))
(define (sum-point p)
  (cond
    [(valid-point? p)
      (+ (point-x p) (point-y p))]
    [else (error "not a valid point! ~a" p)]))

or equivalently you can define the predicate with an explicit Prefab type if you prefer (the two are equivalent):

(define-predicate valid-point? (Prefab point Number Number))

Compatibility across Racket versions

One downside to using define-predicate with a prefab type is that it will only work in Racket versions >= 7.0. If you would like to use this solution but in a way that is also compatible with previous versions of Racket, you can install the prefab-predicate-compat package (e.g. raco pkg install prefab-predicate-compat) and use the following form:

(define-backwards-compatible-flat-prefab-predicate valid-point? point)

This macro inspects the version of Racket which is being used and expands to code that will compile fine in both. In other words, in Racket versions prior to 7.0, it expands into the following:

(define valid-point? point?)

which is clearly the same as just using the (unsound) predicate point? in versions. For versions 7.0 and on it expands into this:

(define-predicate valid-point? point)

Defining a predicate manually

define-predicate uses a flat contract as a predicate. If you're concerned with the performance, it may be worthwhile to define a manual predicate:

(: valid-point? (-> Any Boolean : point))
(define (valid-point? p)
  (and (point? p)
       (number? (point-x p))
       (number? (point-y p))))

Manually defining predicates can sometimes be a little bit tricky, FYI.

Using more specific types

Another alternative is to use more specific types so that, even though the predicate point? doesn't test the values in the fields, it is enough information to determine the value is indeed a point (equivalently (Prefab point Number Number)). This will work well when you know the value is either a point or some other value which is not a (Prefab point Any Any):

(: sum-point (-> (U point False) Number))
(define (sum-point p)
  (cond
    [(point? p)
      (+ (point-x p) (point-y p))]
    [else (error "not a point! ~a" p)]))

I.e. we changed the domain from Any to (U point False), and with that type for the domain, point? returning #true tells us indeed the fields are numbers since the type point is equivalent to (Prefab point Number Number).

(2) Why don't my prefab match clauses work?

The previous example (i.e. sum-point) could also be nicely written using Racket's match macro:

(define (sum-point p)
  (match p
    [(point x y) (+ x y)]
    [_ (error "not a valid point! ~a" p)]))

That would have type checked prior to the 7.0 Racket release. However, for the same reason the manual predicate version breaks, this too will break (i.e. there are no tests for the fields x and y).

In this case, adding predicates for the field patterns is probably the easiest solution:

(: sum-point (-> Any Number))
(define (sum-point p)
  (match p
    [(point (? number? x) (? number? y)) (+ x y)]
    [_ (error "not a valid point! ~a" p)]))

Restricting the domain of the function itself (as the previous section describes) may also solve the issue.

(3) Why don't my prefab field accessor/mutators type check?

All field accessors and mutators are now polymorphic. This is because they work on any value which is the particular prefab, regardless of the values the fields contain.

Unfortunately, this means that some code which used to type check prior to version 7.0:

(: add-xs (-> (Listof point) Number))
(define (add-xs ps)
  (apply + (map point-x ps)))

will now fail to type check because Typed Racket's type inference fails to recognize some combinations of polymorphic operations. E.g., the above example will not error with the following message:

Type Checker: Bad arguments to function in `apply':
Domains: (#(struct:Rest (Number)))*
Arguments:  (Listof Any)
 in: (apply + (map point-x ps))

Mousing over the expression (map point-x ps)in DrRacket indicates it was assigned type (Listof Any), which is not a argument for (apply + ...).

This can be fixed by manually instantiating point-x:

(: add-xs (-> (Listof point) Number))
(define (add-xs ps)
  (apply + (map (inst point-x Number) ps)))

Or a monomorphic version of point-x could be defined (i.e. a non-polymorphic version which expects a (Prefab point Number Number) and returns a Number).