<div dir="ltr">Will andmap work for you?<div><br></div><div><div>   (struct: foo ())</div><div>   (struct: bar ())</div><div>   (define-type FooOrBar (U foo bar))</div><div><br></div><div>   (: f-bar (-> (Listof bar) Void))</div><div>   (define (f-bar xs)</div><div>     (void))</div><div><br></div><div>   (: f-mixed (-> (Listof FooOrBar) Void))</div><div>   (define (f-mixed xs)</div><div>     (void))</div><div><br></div><div>   (: f (-> (Listof FooOrBar) Void))</div><div>   (define (f xs)</div><div>     (if (andmap bar? xs)</div><div>         (f-bar xs) ; contains only bars</div><div>         (f-mixed xs) ; may contain foos as well</div><div>         ))</div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Sep 26, 2014 at 12:07 PM, Konrad Hinsen <span dir="ltr"><<a href="mailto:konrad.hinsen@fastmail.net" target="_blank">konrad.hinsen@fastmail.net</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi everyone,<br>
<br>
I am trying to convince Typed Racket that after a run-time check on<br>
some list, its elements are all of a given type. This is just like<br>
occurrence typing based on a predicate, except that my predicate<br>
is more complicated.<br>
<br>
My first attempt was this:<br>
<br>
<br>
   #lang typed/racket<br>
<br>
   (struct: foo ())<br>
   (struct: bar ())<br>
   (define-type FooOrBar (U foo bar))<br>
<br>
   (: f-bar (-> (Listof bar) Void))<br>
   (define (f-bar xs)<br>
     (void))<br>
<br>
   (: f-mixed (-> (Listof FooOrBar) Void))<br>
   (define (f-mixed xs)<br>
     (void))<br>
<br>
   (: f (-> (Listof FooOrBar) Void))<br>
   (define (f xs)<br>
     (if (for/and : Boolean ([x xs]) (bar? x))<br>
         (f-bar xs) ; contains only bars<br>
         (f-mixed xs) ; may contain foos as well<br>
         ))<br>
<br>
This yields a type error:<br>
<br>
   ; /Users/hinsen/projects/racket/foobar.rkt:18:13: Type Checker: type mismatch<br>
   ;   expected: (Listof bar)<br>
   ;   given: (Listof FooOrBar)<br>
   ;   in: xs<br>
<br>
After reading section 5 of the Typed Racket Guide, in particular section<br>
5.2 entitled "Filters and Predicates", I thought I could simply define my<br>
own predicate with a type annotation:<br>
<br>
   #lang typed/racket<br>
<br>
   (struct: foo ())<br>
   (struct: bar ())<br>
   (define-type FooOrBar (U foo bar))<br>
<br>
   (: f-bar (-> (Listof bar) Void))<br>
   (define (f-bar xs)<br>
     (void))<br>
<br>
   (: f-mixed (-> (Listof FooOrBar) Void))<br>
   (define (f-mixed xs)<br>
     (void))<br>
<br>
   (: pure-bars? (-> (Listof FooOrBar) Boolean : (Listof bar)))<br>
   (define (pure-bars? xs)<br>
     (for/and : Boolean ([x xs]) (bar? x)))<br>
<br>
   (: f (-> (Listof FooOrBar) Void))<br>
   (define (f xs)<br>
     (if (pure-bars? xs)<br>
         (f-bar xs) ; contains only bars<br>
         (f-mixed xs) ; may contain foos as well<br>
         ))<br>
<br>
But this got me only into more trouble - now I don't even understand the<br>
error message any more:<br>
<br>
   ; /Users/hinsen/projects/racket/foobar.rkt:17:2: Type Checker: type mismatch;<br>
   ;  mismatch in filter<br>
   ;   expected: (((Listof bar) @ xs) | (! (Listof bar) @ xs))<br>
   ;   given: (Top | Top)<br>
   ;   in: (for/and : Boolean ((x xs)) (bar? x))<br>
<br>
Is there a way to do this kind of test?<br>
<br>
Konrad.<br>
____________________<br>
  Racket Users list:<br>
  <a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a><br>
</blockquote></div><br></div>