I want to write this piece of code:
(: only-non-false (All (T) ((Listof (U T False)) -> (Listof T))))
(define (only-non-false l)
(filter (ann (lambda (x) x)
((U T False) -> Any : T))
l))
... but Typed Racket says:
Type Checker: Expected result with filter ((T @ x) | (! T @ x)), got filter ((!
False @ x) | (False @ x)) in: x
I'm guessing that Typed Racket isn't clever enough to figure out that when the
input is (U T False), that a filter on not-false is the same as a filter on T.
I gave up on the general case and focused in on the specific one I want, and
ran into another problem where I want subtyping.
Specifically, consider this code:
#lang typed/racket
(: a (Listof (U False (Listof Number))))
(define a '((34) #f (9 22) #f))
(ann (filter pair? a)
(Listof (Listof Number)))
I know that the result is a list of numbers, but that information gets lost...
I suppose the abstraction that I need here would be something like a case on
the right-hand-side of a filter type... oog, no, I think that still wouldn't
help.
I can solve this by refining the predicate so that it matches the (Listof
Number) type exactly, but that seems a bit cumbersome.
Am I missing something obvious in either of these?
Alas, things like this are why TR is *still* in the bin of
"things-I-tackle-when-I'm-not-pressured-for-time".
Thanks!
John
smime.p7s
Description: S/MIME cryptographic signature
____________________ Racket Users list: http://lists.racket-lang.org/users
