[racket] Typed Racket - Setof assertions

On Sat, May 14, 2011 at 1:07 PM, Ray Racine <ray.racine at gmail.com> wrote:
> First I think typed/racket is fantastic.    But when you stray from the
> path, its quicksand. :)

I'm glad you're enjoying it.

> 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?

If you want to define predicates, the best way is to use
`define-predicate'.  For example, for (Listof String):

(define-predicate lststr? (Listof String))

> 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.

Unfortunately, it's not possible to use the contract system usefully
with Typed Racket at the moment.  This is something that I'm looking
into fixing in the near term, though.
-- 
sam th
samth at ccs.neu.edu