[plt-scheme] check-expect and Typed Scheme

Yes. In my "synthesize" view of the world (DLS 2006) this is exactly  
where
they come from. -- Matthias



On Sep 4, 2008, at 9:37 AM, Robby Findler wrote:

> 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
>>
>>