[plt-scheme] Recognizing Listof in typed-scheme

 From: David Van Horn (dvanhorn at ccs.neu.edu) Date: Mon Apr 6 10:20:13 EDT 2009 Previous message: [plt-scheme] Recognizing Listof in typed-scheme Next message: [plt-scheme] Recognizing Listof in typed-scheme Messages sorted by: [date] [thread] [subject] [author]

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

```

 Posted on the users mailing list. Previous message: [plt-scheme] Recognizing Listof in typed-scheme Next message: [plt-scheme] Recognizing Listof in typed-scheme Messages sorted by: [date] [thread] [subject] [author]