[racket] [typed] filters

Thanks, Sam

-- Éric


On Nov 2, 2011, at 7:54 PM, Sam Tobin-Hochstadt wrote:

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