How to fix the return value in this typed racket code?

Question

(: test (All (A) (-> A A (Rec Expr (Listof (U A Expr))) (Rec Expr (Listof (U A Expr))))))
(define (test new old expr)
  (if (null? expr)
      expr
      (if (list? (car expr))
          expr ; <- get error here
          expr)))

get error

Type Checker: type mismatch
expected: (Rec g161252 (Listof (U A g161252)))
given: (Pairof
      (U (Rec g161259 (Listof (U A g161259))) (Pairof Any (Listof Any)))
      (Listof (U A (Rec g161268 (Listof (U A g161268)))))) in: expr

The code return exactly the same expr as the input one.

(define (test new old expr)
  (if (and (not (null? expr)) (list? (car expr)))
      expr ; <- also get the error
      expr))

But

(define (test new old expr)
  (if (and (list? (car expr)) (not (null? expr)))
      expr ; <- this works fine
      expr))

If the logic is in this order, then it works fine.

So why the type checker get the type mismatch error?

It may be helpful to provide a bit more context about the function so that others can more easily understand the code. — ben rudgers
It's just a test function. You can try the code in Racket IDE. The only context is #lang typed/racket — qdwang

Ben Greenman Ben Greenman · Accepted Answer · 2015-11-03T00:25:09

The problem with the original code is that expr is "not polymorphic enough". The query (list? (car expr)) changes the type of expr to something incompatible with the polymorphic A.

(It seems to me that you're trying to discriminate between an A and a nested Expr, but typed racket sees list? and refines the type of A. I think!)

Here's another function that's not polymorphic enough.

(: id (All (A) (-> A A)))
(define (id x)
  (if (boolean? x) x x))

Fixes

If you're on an older version of Racket (v6.2) you can sneak around this with an alias, but that's not a nice thing to do.
```
(: id (All (A) (-> A A)))
(define (id x)
  (define x2 x)
  (if (boolean? x) x2 x)))
```
You can use list-ref instead of car, because list-ref doesn't allow predicates to affect its argument.
```
...
(if (list? (list-ref expr 0))
  expr
  expr)))
```

Change your types a little, so there's a clear way to tell apart A from Expr.

(: test (All (A) (-> A A (Rec Expr (Listof (U (Boxof A) Expr))) (Rec Expr (Listof (U (Boxof A) Expr))))))
(define (test new old expr)
 (if (null? expr)
  expr
  (if (not (box? (car expr)))
   expr
   expr)))

Stop using Typed Racket's polymorphism -- it's too clumsy!

The order issue is because and applies predicates in order, and these predicates destructively change an expression's type. So testing (not (null? expr)) after you've checked (list? (car expr)) forgets that you ever did the first check.

Here's more code with the same issue. We ought to know that expr is non-null and has a list at its head, but Typed Racket's forgotten.

(: test2 (-> (Listof (U (List Natural) Boolean)) Boolean))
(define (test2 expr)
  (if (and (list? (car expr)) (not (null? expr)))
    (= 1 (car (car expr)))
    #f))

This is probably a bug.

How to fix the return value in this typed racket code?

1 Answers