[racket] [typed] filters

On Wed, Nov 2, 2011 at 12:56 PM, Eric Tanter <etanter at dcc.uchile.cl> wrote:
> Hi,
>
> 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?

What's going on here is that Typed Racket isn't smart enough to tell
that if it knows (car p) is Complex, then it should also know that p
is (Pairof Complex ...).  This is something I've wanted to do for a
long time, but haven't gotten done yet.

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

The best thing to do here is to use `define-predicate':

(define-predicate carnum? (Pairof Number Any))
-- 
sam th
samth at ccs.neu.edu