[racket] Tricky case of occurrence typing in Typed Racket

Will andmap work for you?

   (struct: foo ())
   (struct: bar ())
   (define-type FooOrBar (U foo bar))

   (: f-bar (-> (Listof bar) Void))
   (define (f-bar xs)
     (void))

   (: f-mixed (-> (Listof FooOrBar) Void))
   (define (f-mixed xs)
     (void))

   (: f (-> (Listof FooOrBar) Void))
   (define (f xs)
     (if (andmap bar? xs)
         (f-bar xs) ; contains only bars
         (f-mixed xs) ; may contain foos as well
         ))

On Fri, Sep 26, 2014 at 12:07 PM, Konrad Hinsen <konrad.hinsen at fastmail.net>
wrote:

> Hi everyone,
>
> I am trying to convince Typed Racket that after a run-time check on
> some list, its elements are all of a given type. This is just like
> occurrence typing based on a predicate, except that my predicate
> is more complicated.
>
> My first attempt was this:
>
>
>    #lang typed/racket
>
>    (struct: foo ())
>    (struct: bar ())
>    (define-type FooOrBar (U foo bar))
>
>    (: f-bar (-> (Listof bar) Void))
>    (define (f-bar xs)
>      (void))
>
>    (: f-mixed (-> (Listof FooOrBar) Void))
>    (define (f-mixed xs)
>      (void))
>
>    (: f (-> (Listof FooOrBar) Void))
>    (define (f xs)
>      (if (for/and : Boolean ([x xs]) (bar? x))
>          (f-bar xs) ; contains only bars
>          (f-mixed xs) ; may contain foos as well
>          ))
>
> This yields a type error:
>
>    ; /Users/hinsen/projects/racket/foobar.rkt:18:13: Type Checker: type
> mismatch
>    ;   expected: (Listof bar)
>    ;   given: (Listof FooOrBar)
>    ;   in: xs
>
> After reading section 5 of the Typed Racket Guide, in particular section
> 5.2 entitled "Filters and Predicates", I thought I could simply define my
> own predicate with a type annotation:
>
>    #lang typed/racket
>
>    (struct: foo ())
>    (struct: bar ())
>    (define-type FooOrBar (U foo bar))
>
>    (: f-bar (-> (Listof bar) Void))
>    (define (f-bar xs)
>      (void))
>
>    (: f-mixed (-> (Listof FooOrBar) Void))
>    (define (f-mixed xs)
>      (void))
>
>    (: pure-bars? (-> (Listof FooOrBar) Boolean : (Listof bar)))
>    (define (pure-bars? xs)
>      (for/and : Boolean ([x xs]) (bar? x)))
>
>    (: f (-> (Listof FooOrBar) Void))
>    (define (f xs)
>      (if (pure-bars? xs)
>          (f-bar xs) ; contains only bars
>          (f-mixed xs) ; may contain foos as well
>          ))
>
> But this got me only into more trouble - now I don't even understand the
> error message any more:
>
>    ; /Users/hinsen/projects/racket/foobar.rkt:17:2: Type Checker: type
> mismatch;
>    ;  mismatch in filter
>    ;   expected: (((Listof bar) @ xs) | (! (Listof bar) @ xs))
>    ;   given: (Top | Top)
>    ;   in: (for/and : Boolean ((x xs)) (bar? x))
>
> Is there a way to do this kind of test?
>
> Konrad.
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20140926/72332d84/attachment.html>