[racket] Typed Racket - Setof assertions

From: Ray Racine (ray.racine at gmail.com)
Date: Sat May 14 15:57:20 EDT 2011

Sam,

Tried it.  What am I missing?  Thanks.

#lang typed/racket

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

(define-predicate setof-string?  (Setof String))

racket@> ,enter "/code/knozama/fca/src/main/racket/harvest/test.rkt"
test.rkt:19:33: Type Checker: Type (Setof String) could not be converted to
a contract. in: (Setof String)




On Sat, May 14, 2011 at 1:54 PM, Sam Tobin-Hochstadt <samth at ccs.neu.edu>wrote:

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



-- 
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/deaa4e24/attachment.html>

Posted on the users mailing list.