[racket] Typed Racket - Setof assertions

First I think typed/racket is fantastic.    But when you stray from the
path, its quicksand. :)

I'd like to cast / assert  a given (Setof Any) to a (Setof String).

Path #1 - Come up with the following assert predicate.
(: string-set? ((Setof Any) -> Boolean : (Setof String)))

The following approach works for lists but fails to translate.

(: lststr? ((Listof Any) -> Boolean : (Listof String)))
(define (lststr? lst)
 (andmap string? lst))

The quicksand appears to be some sort of constraint on the verifying
procedure to have some sort of magic filter tag on its return value.  How
does one get it there?

Path #2 - Typed uses lots of contracts.  racket/set has a set/c procedure
which allows me to make contract predicates so ...  but I could not any
variation on the following to work, starting with set/c is untyped in
racket/set ... qucksand.

#lang typed/racket

(require
 (except-in racket/set
    set/c))

(require/typed
 racket
 (opaque Contract contract?))

(require/typed
 racket/set
 (set/c ((Any -> Boolean) -> Contract)))

(: string-set? ((Setof Any) -> Boolean : (Setof String)))
 (define (string-set? aset)
   ((set/c string?) aset))

I really don't want to go the route of (Setof Any) -> (Listof Any) ->
(Listof String) -> (Setof String).

Thanks,

Ray








-- 
The object of life is not to be on the side of the majority, but to escape
finding oneself in the ranks of the insane. - Marcus Aurelius
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20110514/c5d9f767/attachment.html>