[racket-dev] Typed Racket and eq?

On Aug 2, 2010, at 10:53 AM, Sam Tobin-Hochstadt wrote:

> On Mon, Aug 2, 2010 at 10:36 AM, Matthias Felleisen
> <matthias at ccs.neu.edu> wrote:
>> 
>> Sam, this is an interesting question and you should look into it because the answer isn't obvious:
>> 
>>  (module A typed/racket (provide map))
>> 
>> passes map from 'somewhere' through A to two contexts: typed and untyped modules. Given that all provides slap on contracts in TR -- that's what the manual says or should say -- it is surprising that this map should ever be the same as the map that came from 'somewhere'.
> 
> The identifier you get for `map' outside this module is the same
> identifier you would have from `racket'.  `provide' adds contracts for
> identifiers *defined in this module* (including those defined by
> `require/typed').  Other modules protect their own code.
> 
>> It certainly wouldn't be the case in a contract world.
> 
> Can you make this more precise?


Let's say 'provide' is a macro in a language L that is specified to add contracts to all names specified, say, 

  (provide/L x) == (provide/contract [x (lambda (x) false)])
  ; silly, I know

When A exports x to B, written in L, and C imports x from B, you get blame for B. 

> 
> (module A racket 
>   (provide/contract [x integer?])
>   (define x 10))
> 
> (module B racket
>   (require 'A)
>   (provide/contract [x (lambda (x) false)]))
> 
> (module C racket 
>   (require 'B)
>   (printf "~s\n" x))
> 
> (require 'C)

;; ---- 

Now, you will say but TR wraps only defined identifiers. I think that is a SUBTLE and INTENSIONAL difference that in principle, a client such as C shouldn't even see. Modules are not supposed to be inspected for who defines what and so on. They are supposed to be service providers will well-defined interfaces. 


Your interface says that all provided identifiers went thru typing and went thru a typed provide interface.