[racket] [typed] filters

From: Eric Tanter (etanter at dcc.uchile.cl)
Date: Wed Nov 2 12:56:10 EDT 2011


Looking at the ICFP'10 paper on logical types, I tried the following:

(: carnum? ((Pairof Any Any) -> Boolean : (Pairof Number Any)))
(define (carnum? p)
  (number? (car p)))

Type Checker: Expected result 
with filter (((Pairof Complex Any) @ p) | (! (Pairof Complex Any) @ p)), 
got filter ((Complex @ (car) p) | (! Complex @ (car) p)) 
in: (number? (car p))

To me, the filters seem to match, though. Any idea what is wrong here?

I want to be able to use carnum? to discriminate <Number,Any> as in:

(: test ((Pairof Any Any) -> Number))
(define (test x)
  (if (carnum? x) (car x)


-- Éric

PS: I'm using version

Posted on the users mailing list.