[racket] filters in typed racket

I tried this:
(: string-with-length-1? (Any -> Boolean : #:+ (String @ 0)))
(define (string-with-length-1? x)
  (if (string? x)
      (one? (string-length x))
      #f))
(declare-refinement string-with-length-1?)
(define-type String-With-Length-1 (Refinement string-with-length-1?))
And it gave me this error:
. Type Checker: parse error in type;
 expected a predicate for argument to Refinement
  given: Nothing in: (Refinement string-with-length-1?)
Even though I declared that string-with-length-1? has the type (Any -> Boolean : #:+ (String @ 0)).

On May 10, 2014, at 12:40 PM, Eric Dobson <eric.n.dobson at gmail.com> wrote:

> The point of Opaque types are that they are opaque and you cannot see
> into them. Thus making them subtypes is against what they are supposed
> to do.
> 
> You want Refinement types which are similar, but get you subtyping.
> They are unsound, and thus are still in experimental. The unsoundness
> is very hard to fix, and thus they likely are not going to leave
> experimental for a while.
> 
> http://www.cs.utah.edu/plt/snapshots/current/doc/ts-reference/Experimental_Features.html
> 
> 
> 
> On Sat, May 10, 2014 at 9:20 AM, Alexander D. Knauth
> <alexander at knauth.org> wrote:
>> 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
>> 
>> 
>> ____________________
>>  Racket Users list:
>>  http://lists.racket-lang.org/users

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20140510/22aa40c9/attachment.html>