[plt-scheme] check-expect and Typed Scheme

I tend to move the inject function into the Typed Scheme
module:


  (: to-keyevent (Any -> KeyEvent))
  (define (to-keyevent x)
    (if (keyevent? x) x (error 'to-keyevent "shouldn't happen: ~s" x)))

  ; later

  (: ke KeyEvent)
  (define ke (to-keyevent 'left))

Sad thing is, though, I had encountered the same situation as
Dave two days before and when I saw it in an email I didn't
recognize it. So perhaps there is room for improvement.

-- Matthias









On Sep 4, 2008, at 8:21 AM, Richard Cobbe wrote:

> On Thu, Sep 04, 2008 at 01:08:03AM -0400, Sam TH wrote:
>
>> So I think the answer is that you're expecting more from Opaque types
>> than they provide.  All they give you is a type that you can check
>> for.  In particular, if you haven't checked for it, it won't ever  
>> be a
>> KeyEvent.  The only ways to construct a KeyEvent are to `require'  
>> one,
>> or test for one with `key-event?'.  So even though (key-event? 'left)
>> is #t, the typechecker doesn't know that.
>>
>> Does that explain what's going on here?
>
> Yes, and this fits with my previous experience with opaque types.   
> But I'm
> curious about the pragmatics of the situation.  The following looks  
> like
> the right idiom to me, but I'm interested in feedback.
>
>     (module source scheme
>
>       (define (key-event? x) ...)
>       (define (inject-key-event x)
>         (if (key-event? x)
>             x
>             (error ...)))
>
>       (provide/contract
>         [key-event? (any? . -> . boolean?)]
>         [inject-key-event (any? . -> . key-event?)]))
>
>     (module client typed-scheme
>
>       (require-opaque-type Key-Event key-event? source)
>       (require/typed inject-key-event (Any -> Key-Event) source)
>
>       ...)
>
> Notes:
>
>   - if you wanted to treat the Key-Event as a Symbol, say, in the
>     client module, you'd probably need a projection function or  
> functions
>     as well.  These would probably just be special-purpose versions  
> of the
>     identity function, at least in this case.
>
>   - depending on the representation of key-events as defined in the  
> source
>     module, you could give `inject-key-event' a more restrictive  
> domain,
>     both in the type and the contract.
>
> Sound reasonable?
>
> Are the contracts and the types redundant?  Consistent?  (I didn't  
> have
> time to actually try this out, so I have no idea if it compiles.)
>
>                                  * * * * *
>
> One of the most interesting things to me about the growth of typed  
> scheme
> is the changes to normal Scheme idioms that it requires.  It's a
> fascinating and occasionally frustrating process to watch as people
> (including myself) try to develop new pragmatic tools for working  
> with the
> new language.
>
> Richard
> _________________________________________________
>   For list-related administrative tasks:
>   http://list.cs.brown.edu/mailman/listinfo/plt-scheme