[racket] Is there a type for a string with length 1?

By the way I would prefer not to use this:
(define (string-with-length-1? x)
  (and (string? x) (one? (string-length x))))
(define-type KeyEvent
  (U (Opaque string-with-length-1?)
     “left”
     “right”
     ...))
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.  

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?  

If there isn’t I can use (Opaque string-with-length-1?), even though I would prefer not to.  

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?

On May 4, 2014, at 8:14 PM, Alexander D. Knauth <alexander at knauth.org> wrote:

> Sorry I hit reply instead of reply all.  
> 
> The docs say that all KeyEvents are strings, but not all strings are KeyEvents.  
> The definition of key-event? says that a key-event is either a string with length 1 or a member of KEY-EVTS.  
> (define (key-event? k) 
>   (and (string? k) (or (= (string-length k) 1) (pair? (member k KEY-EVTS)))))
> KEY-EVTS includes the things like “left” etc.
> I was planning on doing something like this:
> (define-type KeyEvent
>   (U String-with-length-1
>      “left”
>      “right”
>      “up”
>      “down”
>      ...))
> 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.  
> 
> On May 4, 2014, at 7:54 PM, dfeltey at ccs.neu.edu wrote:
> 
>> According to the docs at http://docs.racket-lang.org/teachpack/2htdpuniverse.html?q=type#%28tech._world._keyevent%29 a KeyEvent is just a string. How will you treat keyevents like "left" or "up" in your typed version?
>> 
>> 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.
>> 
>> Dan
>> 
>> 
>> ----- Original Message -----
>> From: "Alexander D. Knauth" <alexander at knauth.org>
>> To: "Racket Users" <users at racket-lang.org>
>> Sent: Sunday, May 4, 2014 7:35:17 PM GMT -05:00 US/Canada Eastern
>> Subject: [racket] Is there a type for a string with length 1?
>> 
>> Is there a type for a string with length 1?  
>> 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.  
>> 
>> 
>> ____________________
>>  Racket Users list:
>>  http://lists.racket-lang.org/users
> 
> ____________________
>  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/20140505/ffd0cb4a/attachment.html>