First I think typed/racket is fantastic.    But when you stray from the path, its quicksand. :)<div><br></div><div>I&#39;d like to cast / assert  a given (Setof Any) to a (Setof String). </div><div><br></div><div>Path #1 - Come up with the following assert predicate.</div>
<div>(: string-set? ((Setof Any) -&gt; Boolean : (Setof String)))</div><div><br></div><div>The following approach works for lists but fails to translate.</div><div><br></div><div><div>(: lststr? ((Listof Any) -&gt; Boolean : (Listof String)))</div>
<div>(define (lststr? lst)</div><div> (andmap string? lst))</div></div><div><div><div><br></div><div>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?</div>
<div><br></div><div>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.</div>
<div><br></div><div><div>#lang typed/racket</div><div><br></div><div>(require </div><div> (except-in racket/set</div><div><span class="Apple-tab-span" style="white-space:pre">        </span>    set/c))</div><div> </div><div>(require/typed</div>
<div> racket</div><div> (opaque Contract contract?))</div><div><br></div><div>(require/typed</div><div> racket/set</div><div> (set/c ((Any -&gt; Boolean) -&gt; Contract)))</div><div><br></div><div>(: string-set? ((Setof Any) -&gt; Boolean : (Setof String)))</div>
<div> (define (string-set? aset)</div><div>   ((set/c string?) aset))</div><div><br></div><div>I really don&#39;t want to go the route of (Setof Any) -&gt; (Listof Any) -&gt; (Listof String) -&gt; (Setof String).   </div>
<div><br></div><div>Thanks,</div><div><br></div><div>Ray</div><div><br></div></div><div> </div><div><br></div><div><br></div><div> </div><div><br></div><div><br></div><div><br></div><div>-- <br>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 <br>

</div></div></div>