[racket] Typed Racket can't filter non-false yet?

On Mon, Jan 30, 2012 at 3:37 PM, Sam Tobin-Hochstadt <samth at ccs.neu.edu> wrote:
> On Mon, Jan 30, 2012 at 3:22 PM, John Clements
> <clements at brinckerhoff.org> wrote:
>> Am I missing something obvious in either of these?
>
> No.  Typed Racket doesn't have type subtraction, which is what you
> need in the first case. I'm not sure why the second case isn't working
> right; I think the type of `filter' is a little too restrictive.

Thinking more about the second case, the problem is that you want the
type of `pair?' to be:

(All (A) (A -> Boolean : A \intersect (Pairof Any Any))

But the type of `pair?' is:

(Any -> Boolean : (Pairof Any Any))

which is equivalent in the first-order case, but not in the
higher-order case, as when used as the argument to `filter'.
-- 
sam th
samth at ccs.neu.edu