[racket] filters in typed racket

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