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

On Mon, Jan 30, 2012 at 3:54 PM, John Clements
<clements at brinckerhoff.org> wrote:
>
> On Jan 30, 2012, at 12:53 PM, Sam Tobin-Hochstadt wrote:
>
>> 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))
>
> Yes, I agree, and intersection types occurred to me in this case too.  I assume you're speaking hypothetically: TR doesn't support intersections, does it?

Right, sorry, that wasn't clear.  Typed Racket doesn't support this
feature.  I think right now you're stuck with the limitations of
higher-order uses of occurrence typing that you've run into.
-- 
sam th
samth at ccs.neu.edu