[plt-scheme] check-expect and Typed Scheme

On Thu, Sep 4, 2008 at 1:03 PM, Carl Eastlund <cce at ccs.neu.edu> wrote:
> 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:

Yes, of course.  I wasn't thinking of those as projections, since
nothing is actually being done to the key-events.  But I guess it all
comes down to what you mean by injections and projections.

-- 
sam th
samth at ccs.neu.edu