[racket-dev] Typed Racket and importing polymorphic code

On Mon, Aug 2, 2010 at 9:42 AM, Shriram Krishnamurthi <sk at cs.brown.edu> wrote:
> Here's a typed module:
>
> (module A typed/racket (provide insert map) (define insert cons))
>
> Here are two clients, which behave inconsistently:
>
>> (module B racket (require 'A) insert)
> . Type Checker: The type of insert cannot be converted to a contract in: insert
>> (module C racket (require 'A) map)
>
> Let's instead save A to a file, and write these clients as:
>
> -----
>
> #lang racket
> (require "typed-set-impl.rkt")
>
> -----
>
> F5 executes fine.  Running works:
>
>> (map + '(1 2 3) '(4 5 6))
> '(5 7 9)
>
> But if I now type at the REPL:
>
>> insert
>
> I get the same error:
>
> Type Checker: The type of insert cannot be converted to a contract in: insert
>
> I have two issues with this:
>
> 1. Why is this discovered only when I "touch" insert and not sooner?
> Is there some kind of lazy contract creation happening at run-time?

This is because of strange interaction between the implementation of
the "Module" language and the implementation of Typed Scheme.  There's
been discussion of how to extend the DrRacket API to fix this bug, but
nothing has come of it yet.

> 1'. That seems unlikely given that if I instead add "insert" to the
> above (#lang racket) source file and run Check Syntax, I get the same
> error -- so it is indeed a static error.  (Well, maybe not "static",
> there are probably three or four "times" at work here.)

This is a different issue - it shouldn't work to use `insert' in an
untyped context, since there's no way to generate a contract for its
type.  This is also what's happening with the REPL, but that shouldn't
be treated as a untyped context (that's the bug).

> 2. Why does the same not happen with map?  I can use map freely; if I
> put it in the #lang racket file and Check Syntax, it draws an arrow
> from map to the required (typed) file.  Yet in the typed file:

`insert' is defined in typed code, and `map' is not.
-- 
sam th
samth at ccs.neu.edu