[racket] filters in typed racket

Well as it turns out it looks like they are broken. In my
experimenting it seems that they only work for functions declared in
the base type environment.

I'm not sure of a solution that will work for you currently.

On Sat, May 10, 2014 at 10:09 AM, Alexander D. Knauth
<alexander at knauth.org> wrote:
> 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
>
>