[plt-scheme] check-expect and Typed Scheme

Should those inject functions be written as assertions? That way typed
scheme can track them better and presumably give better, more uniform
error messages (including source location of the assertion, etc). I'm
thinking of something like:

  (define to-keyevent (assert (-> any/c key-event) (lambda (x) x)))

where "assert" comes from typed scheme (and would be morally
equivalent to defining to-keyevent in a separate module and exporting
it with a contract).

Robby

On Thu, Sep 4, 2008 at 8:31 AM, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
>
> 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
>
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>
>