[racket-dev] Typed Racket and importing polymorphic code

On Mon, Aug 2, 2010 at 9:58 AM, Shriram Krishnamurthi <sk at cs.brown.edu> wrote:
>>> 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).

Sorry, I misread your initial question, and thought something else was
happening.  The bug I was referring to is irrelevant here.

The reason that you don't get an error until you use `insert' is that
the error is only detected when you *use* `insert', not when it's
defined.  This is intentional - otherwise, typed modules would be much
less useful from the untyped side.  It's just as safe, since the error
is still at expansion time.

>>> 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.
>
> Depends on how you want to define the term.  I imported a language
> with map and explicitly provided it.

I mean "defined" in the sense of where the original `define-values' form is.

>  BUT:
>
> That's beside the point.  map has just as much a polymorphic type as
> insert.  You said earlier, "it shouldn't work to use `insert' in an
> untyped context, since there's no way to generate a contract for its
> type".  Why does this statement not apply to map?

No contract is needed for `map' at all - it (like all Racket
primitives) is known to protect itself.
-- 
sam th
samth at ccs.neu.edu