[plt-scheme] check-expect and Typed Scheme

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