[plt-scheme] check-expect and Typed Scheme

From: Sam TH (samth at ccs.neu.edu)
Date: Thu Sep 4 01:08:03 EDT 2008

On Wed, Sep 3, 2008 at 4:12 PM, David Van Horn <dvanhorn at ccs.neu.edu> wrote:
> Matthias Felleisen wrote:
>> No, not yet.
> OK.  On a related note... this doesn't behave as I expected.
> #lang typed-scheme
> (require/opaque-type KeyEvent key-event? htdp/world)
> Welcome to DrScheme, version [3m].
> Language: Module; memory limit: 128 megabytes.
>> key-event?
> - : (Any -> Boolean : ((restrict KeyEvent)) ((remove KeyEvent)))
> #<procedure:pred-cnt>
>> (key-event? 'left)
> - : Boolean
> #t
>> (: k KeyEvent)
>> (define k 'left)
> typecheck: Expected KeyEvent, but got 'left in: (quote left)
> Is this a bug in Typed Scheme, or am I doing something wrong?

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?
sam th
samth at ccs.neu.edu

Posted on the users mailing list.