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 <as...@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 ____________________ Racket Users list: http://lists.racket-lang.org/users
