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
