[racket] filters in typed racket

Then is it possible to make (Opaque string-with-length-1?) a subtype of String, if string-with-length-1? has the type (Any -> Boolean : #:+ (String @ 0))?  

On May 10, 2014, at 11:45 AM, Asumu Takikawa <asumu at ccs.neu.edu> wrote:

> On 2014-05-10 11:30:58 -0400, Alexander D. Knauth wrote:
>>   After trying some stuff and guessing stuff from error messages, and just
>>   to try it and see what happened, I tried this:
>> 
>>   (: string-with-length-1? (Any -> Boolean : #:+ (String @ x) #:- ((U String
>>   Any) @ x)))
>>   (define (string-with-length-1? x)
>>     (if (string? x)
>>         (one? (string-length x))
>>         #f))
>> 
>>   And it gave me this weird error message:
>>   . Type Checker: type mismatch;
>>    mismatch in filter
>>     expected: ((String @ x) | Top)
>>     given: ((String @ x) | Top) in: (if (string? x) (one? (string-length x))
>>   #f)
>>   What?  If it*s expecting ((String @ x) | Top), and I*m giving it ((String
>>   @ x) | Top),  then what*s the problem?
> 
> This works for me if I use the following type declaration instead:
> 
>  (: string-with-length-1? (Any -> Boolean : #:+ (String @ 0) #:- ((U String Any) @ 0)))
> 
> Note that I've switched `x` with `0` in the filters.
> 
> Basically, the formal parameter `x` is not in scope when you write a
> type declaration like this *outside* of the function. If you have a type
> inside the function, it should be in scope.
> 
> The `0` means that you're referring to the 1st parameter, which is `x`.
> 
>>   And is there any documentation anywhere about this?
> 
> There is now, but I just added it a few days ago and it's only in the
> pre-release docs (the syntax may change by v6.0.2):
>  http://www.cs.utah.edu/plt/snapshots/current/doc/ts-reference/type-ref.html?q=#%28form._%28%28lib._typed-racket%2Fbase-env%2Fbase-types-extra..rkt%29._-~3e%29%29
> 
> In the pre-release, you can also write this instead:
> 
>  (: string-with-length-1? (Any -> Boolean : #:+ String))
> 
> which is a shorthand for the type above. It'll also print like that.
> 
> Cheers,
> Asumu