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.hin...@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
>
____________________
Racket Users list:
http://lists.racket-lang.org/users
