[racket-dev] Typed Racket and importing polymorphic code

On Mon, Aug 2, 2010 at 11:14 AM, Shriram Krishnamurthi <sk at cs.brown.edu> wrote:
>
> Okay, so here's another scenario.  This time, TR will NOT just pass
> the value through, as it did map.
>
> ---------------------------------------------------------------- a.rkt
> #lang racket
>
> (define foo 4)
> (provide foo)
> ;; NOTE: a has not done a good job of "protecting" foo,
> ;; whatever the heck that means
> ---------------------------------------------------------------- b.rkt
> #lang typed/racket
>
> (require/typed "a.rkt" [foo Number])
> (provide foo)
> ;; Now I'm going to put an explicit TYPE on foo
> ---------------------------------------------------------------- c.rkt
> #lang racket
>
> (require "b.rkt")
> (string-length foo)
> ----------------------------------------------------------------------
>
> The error message is
>
>  string-length: expects argument of type <string>; given 4
>
> Nothing that looks like a contract violation.
>
> I was willing to live with your previous explanation re. map (whether
> or not it was primitive, the idea that something just passed through).
> But the idea that the typed intermediation above seems to do nothing
> is much harder to defend on similar grounds.

I think this (and your second example, which is the same)  presents an
interesting issue with contracts.  It's not peculiar to types:

#lang racket/load

(module m racket
  (define foo 4) (provide/contract [foo number?]))
(module n racket
  (require 'm) (string-length foo))

Again, no contract error. Right now, this isn't treated as an abuse of
the protected value `4', but as an abuse of `string-length'.  Whether
primitive values should treat function calls on them as "message
sends" and thus be able to respond, potentially with contract errors,
is a really interesting question.  This relates to Cormac's ideas
about proxies for primitive values [1].

[1] http://wiki.ecmascript.org/doku.php?id=harmony:proxies at the
bottom of the page
-- 
sam th
samth at ccs.neu.edu