[plt-scheme] Recognizing Listof in typed-scheme

Paulo J. Matos wrote:
> (: funct (foobar -> foobar1))
> (define (funct f)
>   (match f
>     ((struct foo _)
>      (make-foo1))
>     ((struct bar _)
>      (make-bar1))))
> 
> (: prob (foolist -> foolist1))
> (define (prob fl)
>   (let ([lst (map (lambda: ((f : foo)) (funct f))
>                   (foolist-lst fl))])
>     (make-foolist1 lst)))
> 
> I get:
> typecheck: Wrong function argument type, expected (Listof foo1), got
> (Listof foobar1) for argument 1 in: lst

Is this sufficient?

(: funct* (foobar1 -> foo1))
(define (funct* f)
   (cond [(foo? f) f]
         [else (error "should not happen")]))

(: prob (foolist -> foolist1))
(define (prob fl)
   (let ([lst (map (lambda: ((f : foo)) (funct* (funct f)))
                   (foolist-lst fl))])
     (make-foolist1 lst)))

Basically, you are capable of reasoning that funct always returns a foo1 
when given a foo.  But TS only know that funct goes from (U foo bar) -> 
(U foo1 bar1), which is not enough to conclude that.  The funct* is a 
noop, but convinces TS that the result really is a foo1.

A stronger type you could assign your funct is:

(U (foo -> foo1) (bar -> bar1))

Which would give you the right info, but I don't think TS allows these 
sorts of things:

(: f (U (Number -> Number) (String -> String)))
(define (f x)
   (cond [(number? x) 1]
         [(string? x) "a"]))

David