<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div>I tried this:</div><div><div><font face="Courier New">(: string-with-length-1? (Any -> Boolean : #:+ (String @ 0)))</font></div><div><font face="Courier New">(define (string-with-length-1? x)</font></div><div><font face="Courier New"> (if (string? x)</font></div><div><font face="Courier New"> (one? (string-length x))</font></div><div><font face="Courier New"> #f))</font></div><div><font face="Courier New">(declare-refinement string-with-length-1?)</font></div><div><font face="Courier New">(define-type String-With-Length-1 (Refinement string-with-length-1?))</font></div></div><div>And it gave me this error:</div><div><div><font face="Courier New">. Type Checker: parse error in type;</font></div><div><font face="Courier New"> expected a predicate for argument to Refinement</font></div><div><font face="Courier New"> given: Nothing in: (Refinement string-with-length-1?)</font></div></div><div>Even though I declared that string-with-length-1? has the type <span style="font-family: 'Courier New';">(Any -> Boolean : #:+ (String @ 0))</span>.</div><div><br></div><div><div><div>On May 10, 2014, at 12:40 PM, Eric Dobson <<a href="mailto:eric.n.dobson@gmail.com">eric.n.dobson@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite">The point of Opaque types are that they are opaque and you cannot see<br>into them. Thus making them subtypes is against what they are supposed<br>to do.<br><br>You want Refinement types which are similar, but get you subtyping.<br>They are unsound, and thus are still in experimental. The unsoundness<br>is very hard to fix, and thus they likely are not going to leave<br>experimental for a while.<br><br><a href="http://www.cs.utah.edu/plt/snapshots/current/doc/ts-reference/Experimental_Features.html">http://www.cs.utah.edu/plt/snapshots/current/doc/ts-reference/Experimental_Features.html</a><br><br><br><br>On Sat, May 10, 2014 at 9:20 AM, Alexander D. Knauth<br><alexander@knauth.org> wrote:<br><blockquote type="cite">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))?<br><br>On May 10, 2014, at 11:45 AM, Asumu Takikawa <asumu@ccs.neu.edu> wrote:<br><br><blockquote type="cite">On 2014-05-10 11:30:58 -0400, Alexander D. Knauth wrote:<br><blockquote type="cite"> After trying some stuff and guessing stuff from error messages, and just<br> to try it and see what happened, I tried this:<br><br> (: string-with-length-1? (Any -> Boolean : #:+ (String @ x) #:- ((U String<br> Any) @ x)))<br> (define (string-with-length-1? x)<br> (if (string? x)<br> (one? (string-length x))<br> #f))<br><br> And it gave me this weird error message:<br> . Type Checker: type mismatch;<br> mismatch in filter<br> expected: ((String @ x) | Top)<br> given: ((String @ x) | Top) in: (if (string? x) (one? (string-length x))<br> #f)<br> What? If it*s expecting ((String @ x) | Top), and I*m giving it ((String<br> @ x) | Top), then what*s the problem?<br></blockquote><br>This works for me if I use the following type declaration instead:<br><br> (: string-with-length-1? (Any -> Boolean : #:+ (String @ 0) #:- ((U String Any) @ 0)))<br><br>Note that I've switched `x` with `0` in the filters.<br><br>Basically, the formal parameter `x` is not in scope when you write a<br>type declaration like this *outside* of the function. If you have a type<br>inside the function, it should be in scope.<br><br>The `0` means that you're referring to the 1st parameter, which is `x`.<br><br><blockquote type="cite"> And is there any documentation anywhere about this?<br></blockquote><br>There is now, but I just added it a few days ago and it's only in the<br>pre-release docs (the syntax may change by v6.0.2):<br> 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<br><br>In the pre-release, you can also write this instead:<br><br> (: string-with-length-1? (Any -> Boolean : #:+ String))<br><br>which is a shorthand for the type above. It'll also print like that.<br><br>Cheers,<br>Asumu<br></blockquote><br><br>____________________<br> Racket Users list:<br> http://lists.racket-lang.org/users<br></blockquote></blockquote></div><br></div></body></html>