[plt-scheme] check-expect and Typed Scheme

On Thu, Sep 4, 2008 at 12:30 PM, Sam TH <samth at ccs.neu.edu> wrote:
> On Thu, Sep 4, 2008 at 10:40 AM, Richard Cobbe <cobbe at ccs.neu.edu> wrote:
>>
>> Oh, of course.  I'd forgotten that Typed Scheme uses the predicate in the
>> conditional to restrict the type of x in the first branch of the if.  Given
>> that, putting the injection functions into the typed module makes sense,
>> because untyped clients are unlikely to use them (especially if the untyped
>> modules use contracts).
>>
>> Can you write the projections in Typed Scheme, though?  Or do those still
>> have to be in the untyped world?
>
> Most likely not.  The only operations you have on an opaque type are
> ones you require from other modules, so any project would have to be
> imported.

No, you also have operations defined on all types, such as predicates.
 The following typechecks just fine, and runs without error:

#lang typed-scheme
(require/opaque-type KeyEvent key-event? htdp/world)

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

(: to-symbol (KeyEvent -> Symbol))
(define (to-symbol ke)
  (if (symbol? ke)
      ke
      (error 'to-symbol "not a symbol: ~s" ke)))

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

(: sym Symbol)
(define sym (to-symbol ke))

-- 
Carl Eastlund