<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div>By the way I would prefer not to use this:</div><div><font face="Courier New">(define (string-with-length-1? x)</font></div><div><font face="Courier New"> (and (string? x) (one? (string-length x))))</font></div><div><font face="Courier New">(define-type KeyEvent</font></div><div><font face="Courier New"> (U (Opaque string-with-length-1?)</font></div><div><font face="Courier New"> “left”</font></div><div><font face="Courier New"> “right”</font></div><div><font face="Courier New"> ...))</font></div><div>because then it can’t tell that it’s a subtype of String, and also it can’t tell that a string is a KeyEvent unless I use (cast “a” KeyEvent) or (assert “a” key-event?) or something like that. </div><div><br></div><div>And if there isn’t a type for a string with length 1, then is there a type constructor that’s sort of like (String-With Char …), where “abcd” could have the type (String-With #\a #\b #\c #\d), and a string with length 1 could have the type (String-With Char), maybe? </div><div><br></div><div>If there isn’t I can use (Opaque string-with-length-1?), even though I would prefer not to. </div><div><br></div><div>By the way is there a way of specifying filters so that it knows that if (string-with-length-1? x) returns true, it knows that x is a String, but it doesn’t mean that if it returns false it’s not a string? And if there is, then could (Opaque string-with-length-1?) be a subtype of String?</div><br><div><div>On May 4, 2014, at 8:14 PM, Alexander D. Knauth <<a href="mailto:alexander@knauth.org">alexander@knauth.org</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><meta http-equiv="Content-Type" content="text/html charset=windows-1252"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><meta http-equiv="Content-Type" content="text/html charset=windows-1252"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div>Sorry I hit reply instead of reply all. </div><div><br></div><div>The docs say that all KeyEvents are strings, but not all strings are KeyEvents. </div><div>The definition of key-event? says that a key-event is either a string with length 1 or a member of KEY-EVTS. </div><div><div>(define (key-event? k) </div><div> (and (string? k) (or (= (string-length k) 1) (pair? (member k KEY-EVTS)))))</div></div><div>KEY-EVTS includes the things like “left” etc.</div><div>I was planning on doing something like this:</div><div><font face="Courier New">(define-type KeyEvent</font></div><div><font face="Courier New"> (U String-with-length-1</font></div><div><font face="Courier New"> “left”</font></div><div><font face="Courier New"> “right”</font></div><div><font face="Courier New"> “up”</font></div><div><font face="Courier New"> “down”</font></div><div><font face="Courier New"> ...))</font></div><div>I don’t want to use the Char type (or something like (U Char “left” “right” …)) because I want all of the key handlers etc. that worked for the big-bang from 2htdp/universe to work for my version. </div><br><div><div>On May 4, 2014, at 7:54 PM, <a href="mailto:dfeltey@ccs.neu.edu">dfeltey@ccs.neu.edu</a> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite">According to the docs at <a href="http://docs.racket-lang.org/teachpack/2htdpuniverse.html?q=type#%28tech._world._keyevent%29">http://docs.racket-lang.org/teachpack/2htdpuniverse.html?q=type#%28tech._world._keyevent%29</a> a KeyEvent is just a string. How will you treat keyevents like "left" or "up" in your typed version?<br><br>There is a Char type, but would rule out things like "left", "right", "up", "down". You could just use String as your type and define constructors that ensure the string passed in is actually a KeyEvent.<br><br>Dan<br><br><br>----- Original Message -----<br>From: "Alexander D. Knauth" <<a href="mailto:alexander@knauth.org">alexander@knauth.org</a>><br>To: "Racket Users" <<a href="mailto:users@racket-lang.org">users@racket-lang.org</a>><br>Sent: Sunday, May 4, 2014 7:35:17 PM GMT -05:00 US/Canada Eastern<br>Subject: [racket] Is there a type for a string with length 1?<br><br>Is there a type for a string with length 1? <br>The reason is that I’m trying to make my own typed version of big-bang and I want to make a type for KeyEvent. <br><br><br>____________________<br> Racket Users list:<br> <a href="http://lists.racket-lang.org/users">http://lists.racket-lang.org/users</a><br></blockquote></div><br></div></div>____________________<br> Racket Users list:<br> <a href="http://lists.racket-lang.org/users">http://lists.racket-lang.org/users</a><br></blockquote></div><br></body></html>