[racket] filters in typed racket

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