Re: [racket-dev] Typed Racket and importing polymorphic code
On Mon, Aug 2, 2010 at 9:58 AM, Shriram Krishnamurthi s...@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 sa...@ccs.neu.edu _ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
Re: [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 sa...@ccs.neu.edu wrote: On Mon, Aug 2, 2010 at 11:14 AM, Shriram Krishnamurthi s...@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 sa...@ccs.neu.edu _ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
