[racket-dev] Typed Racket and importing polymorphic code

Arjun just pointed out to me that the inability to contract base
values can lead to much harder-to-understand problems in higher-order
contexts.  (Not surprising, but I hadn't thought that that would make
it much worse.)

On Mon, Aug 2, 2010 at 11:44 AM, Sam Tobin-Hochstadt <samth at ccs.neu.edu> wrote:
> 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
>