Re: [racket-dev] Machinery for eliding contracts
Yes, I think this would allow all the optimizations that Eric talked about. Sam On Jun 13, 2014 4:26 AM, Robby Findler ro...@eecs.northwestern.edu wrote: Would it be useful to get blame information back from a value, just like you can currently get the contract back? Robby On Tue, Jun 10, 2014 at 11:53 AM, Matthias Felleisen matth...@ccs.neu.edu wrote: I was thinking of associating the contract with the type from which it comes and no that's not hash-consing. And if it's slower, too bad. -- Matthias On Jun 10, 2014, at 12:47 PM, Eric Dobson eric.n.dob...@gmail.com wrote: On Tue, Jun 10, 2014 at 6:15 AM, Matthias Felleisen matth...@ccs.neu.edu wrote: On Jun 9, 2014, at 6:02 PM, Eric Dobson eric.n.dob...@gmail.com wrote: Eric, are you talking about changing the proxy values that wrap HO/mutable contracted values? Yes. I want the proxy values to include information about who agreed to the contract in addition to the contract agreed to. I actually realize that I might need more than just the contract agreed to because of how TR changes the generated contract to remove checks for what it guarantees, so that info is not in the contract. But I believe that can be added back as a structure property on the contract. Would some form of hash-consing contracts work here? -- Matthias I don't think so. But not sure exactly what you are proposing. The issue is that there are 4 contracts here and 2 of them currently do not exist at runtime. The 4 are TRs checks/promises on an export/import. (Using import for a value flowing into an exported function). The promise contracts do not currently exist as removing them was my previous optimization (They never fail). What I want to do is change the check on import from (array/c symbol?) to (if/c (protected? (array/c symbol?)) any/c (array/c symbol?)). Where (protected? x/c) checks if TR already promised something stronger than x/c. I believe that you are proposing that we can use the identity of the contract returned by value-contract to determine what the promised contract would have been. This does not work as (Array Symbol) and (Array Float) both get translated to (array/c any/c) for export, and we would want to lookup different promised contracts for them. We could use weak hash map as an extra field but that seems like it would be slow. _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Machinery for eliding contracts
You also can't protect against someone using the FFI to fake whatever value you thought was safe. I think your best bet here is to document what you're doing any why you're doing it and then treat uses of some primitive things (like directly constructing blame records in this case) as unsafe operations. Robby On Fri, Jun 13, 2014 at 10:32 AM, Eric Dobson eric.n.dob...@gmail.com wrote: I believe thats what I need for the optimization-half, but I don't think it allows for soundly implementing the optimizations. I still don't see how to test if a value came from TR instead of someone trying to fake that, especially if they can get the blame object from one export and reuse it on a different value. On Fri, Jun 13, 2014 at 6:29 AM, Robby Findler ro...@eecs.northwestern.edu wrote: Okay, I'll push has-blame? and value-blame. Let me know if there are any problems. Robby On Fri, Jun 13, 2014 at 5:59 AM, Sam Tobin-Hochstadt sa...@cs.indiana.edu wrote: Yes, I think this would allow all the optimizations that Eric talked about. Sam On Jun 13, 2014 4:26 AM, Robby Findler ro...@eecs.northwestern.edu wrote: Would it be useful to get blame information back from a value, just like you can currently get the contract back? Robby On Tue, Jun 10, 2014 at 11:53 AM, Matthias Felleisen matth...@ccs.neu.edu wrote: I was thinking of associating the contract with the type from which it comes and no that's not hash-consing. And if it's slower, too bad. -- Matthias On Jun 10, 2014, at 12:47 PM, Eric Dobson eric.n.dob...@gmail.com wrote: On Tue, Jun 10, 2014 at 6:15 AM, Matthias Felleisen matth...@ccs.neu.edu wrote: On Jun 9, 2014, at 6:02 PM, Eric Dobson eric.n.dob...@gmail.com wrote: Eric, are you talking about changing the proxy values that wrap HO/mutable contracted values? Yes. I want the proxy values to include information about who agreed to the contract in addition to the contract agreed to. I actually realize that I might need more than just the contract agreed to because of how TR changes the generated contract to remove checks for what it guarantees, so that info is not in the contract. But I believe that can be added back as a structure property on the contract. Would some form of hash-consing contracts work here? -- Matthias I don't think so. But not sure exactly what you are proposing. The issue is that there are 4 contracts here and 2 of them currently do not exist at runtime. The 4 are TRs checks/promises on an export/import. (Using import for a value flowing into an exported function). The promise contracts do not currently exist as removing them was my previous optimization (They never fail). What I want to do is change the check on import from (array/c symbol?) to (if/c (protected? (array/c symbol?)) any/c (array/c symbol?)). Where (protected? x/c) checks if TR already promised something stronger than x/c. I believe that you are proposing that we can use the identity of the contract returned by value-contract to determine what the promised contract would have been. This does not work as (Array Symbol) and (Array Float) both get translated to (array/c any/c) for export, and we would want to lookup different promised contracts for them. We could use weak hash map as an extra field but that seems like it would be slow. _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Machinery for eliding contracts
On Jun 9, 2014, at 6:02 PM, Eric Dobson eric.n.dob...@gmail.com wrote: Eric, are you talking about changing the proxy values that wrap HO/mutable contracted values? Yes. I want the proxy values to include information about who agreed to the contract in addition to the contract agreed to. I actually realize that I might need more than just the contract agreed to because of how TR changes the generated contract to remove checks for what it guarantees, so that info is not in the contract. But I believe that can be added back as a structure property on the contract. Would some form of hash-consing contracts work here? -- Matthias smime.p7s Description: S/MIME cryptographic signature _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Machinery for eliding contracts
On Tue, Jun 10, 2014 at 6:15 AM, Matthias Felleisen matth...@ccs.neu.edu wrote: On Jun 9, 2014, at 6:02 PM, Eric Dobson eric.n.dob...@gmail.com wrote: Eric, are you talking about changing the proxy values that wrap HO/mutable contracted values? Yes. I want the proxy values to include information about who agreed to the contract in addition to the contract agreed to. I actually realize that I might need more than just the contract agreed to because of how TR changes the generated contract to remove checks for what it guarantees, so that info is not in the contract. But I believe that can be added back as a structure property on the contract. Would some form of hash-consing contracts work here? -- Matthias I don't think so. But not sure exactly what you are proposing. The issue is that there are 4 contracts here and 2 of them currently do not exist at runtime. The 4 are TRs checks/promises on an export/import. (Using import for a value flowing into an exported function). The promise contracts do not currently exist as removing them was my previous optimization (They never fail). What I want to do is change the check on import from (array/c symbol?) to (if/c (protected? (array/c symbol?)) any/c (array/c symbol?)). Where (protected? x/c) checks if TR already promised something stronger than x/c. I believe that you are proposing that we can use the identity of the contract returned by value-contract to determine what the promised contract would have been. This does not work as (Array Symbol) and (Array Float) both get translated to (array/c any/c) for export, and we would want to lookup different promised contracts for them. We could use weak hash map as an extra field but that seems like it would be slow. _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Machinery for eliding contracts
I was thinking of associating the contract with the type from which it comes and no that's not hash-consing. And if it's slower, too bad. -- Matthias On Jun 10, 2014, at 12:47 PM, Eric Dobson eric.n.dob...@gmail.com wrote: On Tue, Jun 10, 2014 at 6:15 AM, Matthias Felleisen matth...@ccs.neu.edu wrote: On Jun 9, 2014, at 6:02 PM, Eric Dobson eric.n.dob...@gmail.com wrote: Eric, are you talking about changing the proxy values that wrap HO/mutable contracted values? Yes. I want the proxy values to include information about who agreed to the contract in addition to the contract agreed to. I actually realize that I might need more than just the contract agreed to because of how TR changes the generated contract to remove checks for what it guarantees, so that info is not in the contract. But I believe that can be added back as a structure property on the contract. Would some form of hash-consing contracts work here? -- Matthias I don't think so. But not sure exactly what you are proposing. The issue is that there are 4 contracts here and 2 of them currently do not exist at runtime. The 4 are TRs checks/promises on an export/import. (Using import for a value flowing into an exported function). The promise contracts do not currently exist as removing them was my previous optimization (They never fail). What I want to do is change the check on import from (array/c symbol?) to (if/c (protected? (array/c symbol?)) any/c (array/c symbol?)). Where (protected? x/c) checks if TR already promised something stronger than x/c. I believe that you are proposing that we can use the identity of the contract returned by value-contract to determine what the promised contract would have been. This does not work as (Array Symbol) and (Array Float) both get translated to (array/c any/c) for export, and we would want to lookup different promised contracts for them. We could use weak hash map as an extra field but that seems like it would be slow. _ Racket Developers list: http://lists.racket-lang.org/dev
[racket-dev] Machinery for eliding contracts
One of the slowest parts when using TR is the contract boundary between untyped and typed code. Even with recent changes it still causes a large overhead. Example: #lang racket/load (module lib typed/racket (provide f g) (: f (Symbol - (Boxof Symbol))) (define (f x) (box x)) (: g ((Boxof Symbol) - Symbol)) (define (g x) (unbox x))) (module user-1 racket (provide go1) (require 'lib) (define (go1) (for ((i (in-range 20))) (g (f 'x) (module user-2 typed/racket (provide go2) (require 'lib) (define (go2) (for ((i (in-range 1))) (g (f 'x) (require 'user-1 'user-2) (for ((j 5)) (time (go1)) (time (go2))) It would be nice if the contract on the input to g could be elided. It seems like this could be done by using something like prop:contracted but that allowed accessing the parties that agreed to the contract. I'm imagining something like (lambda (v) (and (has-contract? v) (contracted-value-providing-side=? v 'the-typed-world) (contract-stronger? (value-contract v) new-contract))) One issue I see is that we need an unforgeable property that the value actually came from the typed world so we know that eliding the new contract is safe. Does this seem like a reasonable thing to support/do people see issues with it? Other related ideas I had were: A similar thing could be done if the same contract were being applied multiple times with the same blame parties. In that case the later contracts could be elided because they would error out in exactly the same cases with exactly the same messages. That in addition to not applying the new contract if it is weaker than the old contract, we remove the old contract (and access the unprotected value) if the new contract is stronger. In the case that they were the same contract this would mean that there would be no higher order contract checks while the typed code was executing. _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Machinery for eliding contracts
Am I right that the contract on 'f' is actually (- symbol? any)? And if so, where is the information coming from that lets you elide the check? One idea for this particular case: make 'g' be a macro that inspects its argument and if it see obvious things like this, then it can expand into a call to an unprotected use of 'g' instead of the protected one. I'm not sure how general this would be, tho, but it has two advantages: a) it can be done at compile time and b) it doesn't need to deal with arbitrary contracts, only the ones generated by types. Does that approach seem to have enough merit? Robby On Mon, Jun 9, 2014 at 2:19 AM, Eric Dobson eric.n.dob...@gmail.com wrote: One of the slowest parts when using TR is the contract boundary between untyped and typed code. Even with recent changes it still causes a large overhead. Example: #lang racket/load (module lib typed/racket (provide f g) (: f (Symbol - (Boxof Symbol))) (define (f x) (box x)) (: g ((Boxof Symbol) - Symbol)) (define (g x) (unbox x))) (module user-1 racket (provide go1) (require 'lib) (define (go1) (for ((i (in-range 20))) (g (f 'x) (module user-2 typed/racket (provide go2) (require 'lib) (define (go2) (for ((i (in-range 1))) (g (f 'x) (require 'user-1 'user-2) (for ((j 5)) (time (go1)) (time (go2))) It would be nice if the contract on the input to g could be elided. It seems like this could be done by using something like prop:contracted but that allowed accessing the parties that agreed to the contract. I'm imagining something like (lambda (v) (and (has-contract? v) (contracted-value-providing-side=? v 'the-typed-world) (contract-stronger? (value-contract v) new-contract))) One issue I see is that we need an unforgeable property that the value actually came from the typed world so we know that eliding the new contract is safe. Does this seem like a reasonable thing to support/do people see issues with it? Other related ideas I had were: A similar thing could be done if the same contract were being applied multiple times with the same blame parties. In that case the later contracts could be elided because they would error out in exactly the same cases with exactly the same messages. That in addition to not applying the new contract if it is weaker than the old contract, we remove the old contract (and access the unprotected value) if the new contract is stronger. In the case that they were the same contract this would mean that there would be no higher order contract checks while the typed code was executing. _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Machinery for eliding contracts
On Mon, Jun 9, 2014 at 5:48 AM, Robby Findler ro...@eecs.northwestern.edu wrote: Am I right that the contract on 'f' is actually (- symbol? any)? And if so, where is the information coming from that lets you elide the check? No, the `(boxof symbol?)` contract has to be kept around because of mutability. One idea for this particular case: make 'g' be a macro that inspects its argument and if it see obvious things like this, then it can expand into a call to an unprotected use of 'g' instead of the protected one. I'm not sure how general this would be, tho, but it has two advantages: a) it can be done at compile time and b) it doesn't need to deal with arbitrary contracts, only the ones generated by types. Does that approach seem to have enough merit? I don't understand how this is supposed to work. If `g` was a macro, how would it know that `f` was something it could specialize on? Would every TR export also have some static information about its contract so that macros like `g` could recognize them? Sam Robby On Mon, Jun 9, 2014 at 2:19 AM, Eric Dobson eric.n.dob...@gmail.com wrote: One of the slowest parts when using TR is the contract boundary between untyped and typed code. Even with recent changes it still causes a large overhead. Example: #lang racket/load (module lib typed/racket (provide f g) (: f (Symbol - (Boxof Symbol))) (define (f x) (box x)) (: g ((Boxof Symbol) - Symbol)) (define (g x) (unbox x))) (module user-1 racket (provide go1) (require 'lib) (define (go1) (for ((i (in-range 20))) (g (f 'x) (module user-2 typed/racket (provide go2) (require 'lib) (define (go2) (for ((i (in-range 1))) (g (f 'x) (require 'user-1 'user-2) (for ((j 5)) (time (go1)) (time (go2))) It would be nice if the contract on the input to g could be elided. It seems like this could be done by using something like prop:contracted but that allowed accessing the parties that agreed to the contract. I'm imagining something like (lambda (v) (and (has-contract? v) (contracted-value-providing-side=? v 'the-typed-world) (contract-stronger? (value-contract v) new-contract))) One issue I see is that we need an unforgeable property that the value actually came from the typed world so we know that eliding the new contract is safe. Does this seem like a reasonable thing to support/do people see issues with it? Other related ideas I had were: A similar thing could be done if the same contract were being applied multiple times with the same blame parties. In that case the later contracts could be elided because they would error out in exactly the same cases with exactly the same messages. That in addition to not applying the new contract if it is weaker than the old contract, we remove the old contract (and access the unprotected value) if the new contract is stronger. In the case that they were the same contract this would mean that there would be no higher order contract checks while the typed code was executing. _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Machinery for eliding contracts
On Mon, Jun 9, 2014 at 3:19 AM, Eric Dobson eric.n.dob...@gmail.com wrote: It would be nice if the contract on the input to g could be elided. It seems like this could be done by using something like prop:contracted but that allowed accessing the parties that agreed to the contract. I'm imagining something like (lambda (v) (and (has-contract? v) (contracted-value-providing-side=? v 'the-typed-world) (contract-stronger? (value-contract v) new-contract))) One issue I see is that we need an unforgeable property that the value actually came from the typed world so we know that eliding the new contract is safe. Does this seem like a reasonable thing to support/do people see issues with it? It seems like this could be simplified a little just by allowing contract parties to be compared. IOW, at the point where you're writing that function, we have two contracts, and we need to know if the negative party of one is the positive party of the other. Then you don't need to worry about unforgeability, I think. Sam _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Machinery for eliding contracts
On 06/09/2014 01:19 AM, Eric Dobson wrote: Does this seem like a reasonable thing to support/do people see issues with it? I can only speak on reasonableness, and my answer is emphatically YES. Typed Racket is a great language in which to define and use data structures: access is very fast, and many properties are checked statically. But accessor performance suffers badly when the data types are used in untyped Racket. If access uses higher-order functions (e.g. math/array), wrapping the functions slows access by a very high constant factor. If the data structures are first-order, every O(1) access becomes O(n). I recently had to work around this in Plot when I needed an untyped module to be able to operate on typed BSP trees. I ended up making a typed weak hash map from BSP tree handles (gensyms) to BSP trees, and writing a new untyped API for operating on trees using handles. It was ugly. If the untyped and typed modules had been too tightly coupled, it would have been impossible. IIUC, your proposal would make untyped use of typed data structures actually feasible for real-world use. So again, YES. Neil ⊥ _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Machinery for eliding contracts
On 06/09/2014 10:25 AM, Neil Toronto wrote: On 06/09/2014 01:19 AM, Eric Dobson wrote: Does this seem like a reasonable thing to support/do people see issues with it? I can only speak on reasonableness, and my answer is emphatically YES. Typed Racket is a great language in which to define and use data structures: access is very fast, and many properties are checked statically. But accessor performance suffers badly when the data types are used in untyped Racket. If access uses higher-order functions (e.g. math/array), wrapping the functions slows access by a very high constant factor. If the data structures are first-order, every O(1) access becomes O(n). I recently had to work around this in Plot when I needed an untyped module to be able to operate on typed BSP trees. I ended up making a typed weak hash map from BSP tree handles (gensyms) to BSP trees, and writing a new untyped API for operating on trees using handles. It was ugly. If the untyped and typed modules had been too tightly coupled, it would have been impossible. IIUC, your proposal would make untyped use of typed data structures actually feasible for real-world use. So again, YES. Here's a concrete example, using Typed Racket to define a new list type. #lang racket (module typed-defs typed/racket (provide list-my-list my-first) (define-type (My-Listof A) (U Null (my-cons A))) (struct (A) my-cons ([fst : A] [snd : (My-Listof A)]) #:transparent) (: list-my-list (All (A) (- (Listof A) (My-Listof A (define (list-my-list xs) (if (empty? xs) xs (my-cons (first xs) (list-my-list (rest xs) (: my-first (All (A) (- (My-Listof A) A))) (define (my-first xs) (if (empty? xs) (error 'bad) (my-cons-fst xs))) ;; Timing loop speed is very fast and O(1) (define lst (list-my-list '(1))) (for ([_ (in-range 5)]) (time (for ([_ (in-range 100)]) (my-first lst ) (require 'typed-defs) ;; Timing loop speed is very slow and O(n) (define lst (list-my-list '(1))) (for ([_ (in-range 5)]) (time (for ([_ (in-range 100)]) (my-first lst I get 4ms for the timing loop in the typed module, and 620ms for the timing loop in the untyped module, so the constant factor is about 150. When I change the test data from '(1) to '(1 2), the untyped module's timing loop takes about 1010ms. The contract boundary has changed the asymptotic complexity of `my-first' from O(1) to O(n). Neil ⊥ _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Machinery for eliding contracts
On 2014-06-09 00:19:40 -0700, Eric Dobson wrote: One issue I see is that we need an unforgeable property that the value actually came from the typed world so we know that eliding the new contract is safe. Does this seem like a reasonable thing to support/do people see issues with it? A potentially useful generalization of this that's not just for TR is to avoid duplicate complex check ons values (no types involved), making complicated contracts more feasible. Imagine a contract that parses a string to see if it is a valid IP address, for example. Would this only work for higher-order/behavioral values/types though? (i.e., not my IP example) Cheers, Asumu _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Machinery for eliding contracts
On Jun 9, 2014, at 9:38 AM, Sam Tobin-Hochstadt sa...@cs.indiana.edu wrote: On Mon, Jun 9, 2014 at 3:19 AM, Eric Dobson eric.n.dob...@gmail.com wrote: It would be nice if the contract on the input to g could be elided. It seems like this could be done by using something like prop:contracted but that allowed accessing the parties that agreed to the contract. I'm imagining something like (lambda (v) (and (has-contract? v) (contracted-value-providing-side=? v 'the-typed-world) (contract-stronger? (value-contract v) new-contract))) One issue I see is that we need an unforgeable property that the value actually came from the typed world so we know that eliding the new contract is safe. Does this seem like a reasonable thing to support/do people see issues with it? It seems like this could be simplified a little just by allowing contract parties to be compared. IOW, at the point where you're writing that function, we have two contracts, and we need to know if the negative party of one is the positive party of the other. Then you don't need to worry about unforgeability, I think. Well some code could swap identities on such things. Not accidentally. Plus I think this would eliminate the anticipated benefits if there are chains of TR modules involved. I think Eric just needs to know whether something came out of the TR world and flows back w/o being touched. ;; --- Eric, are you talking about changing the proxy values that wrap HO/mutable contracted values? -- Matthias smime.p7s Description: S/MIME cryptographic signature _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Machinery for eliding contracts
On Mon, Jun 9, 2014 at 8:35 AM, Sam Tobin-Hochstadt sa...@cs.indiana.edu wrote: On Mon, Jun 9, 2014 at 5:48 AM, Robby Findler ro...@eecs.northwestern.edu wrote: Am I right that the contract on 'f' is actually (- symbol? any)? And if so, where is the information coming from that lets you elide the check? No, the `(boxof symbol?)` contract has to be kept around because of mutability. One idea for this particular case: make 'g' be a macro that inspects its argument and if it see obvious things like this, then it can expand into a call to an unprotected use of 'g' instead of the protected one. I'm not sure how general this would be, tho, but it has two advantages: a) it can be done at compile time and b) it doesn't need to deal with arbitrary contracts, only the ones generated by types. Does that approach seem to have enough merit? I don't understand how this is supposed to work. If `g` was a macro, how would it know that `f` was something it could specialize on? Would every TR export also have some static information about its contract so that macros like `g` could recognize them? Well, I was thinking it would have static information about its type, actually. But yes. Robby _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Machinery for eliding contracts
On Mon, Jun 9, 2014 at 8:38 AM, Sam Tobin-Hochstadt sa...@cs.indiana.edu wrote: On Mon, Jun 9, 2014 at 3:19 AM, Eric Dobson eric.n.dob...@gmail.com wrote: It would be nice if the contract on the input to g could be elided. It seems like this could be done by using something like prop:contracted but that allowed accessing the parties that agreed to the contract. I'm imagining something like (lambda (v) (and (has-contract? v) (contracted-value-providing-side=? v 'the-typed-world) (contract-stronger? (value-contract v) new-contract))) One issue I see is that we need an unforgeable property that the value actually came from the typed world so we know that eliding the new contract is safe. Does this seem like a reasonable thing to support/do people see issues with it? It seems like this could be simplified a little just by allowing contract parties to be compared. IOW, at the point where you're writing that function, we have two contracts, and we need to know if the negative party of one is the positive party of the other. Then you don't need to worry about unforgeability, I think. Yes, I think you'd just need to compare the blame parties (and equal? should be fine for that). Altho you would need to know that the contract came from the contract library to trust it, but that trust would be built into the contract-stronger? predicate. Robby _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Machinery for eliding contracts
On Mon, Jun 9, 2014 at 8:35 AM, Sam Tobin-Hochstadt sa...@cs.indiana.edu wrote: On Mon, Jun 9, 2014 at 5:48 AM, Robby Findler ro...@eecs.northwestern.edu wrote: Am I right that the contract on 'f' is actually (- symbol? any)? And if so, where is the information coming from that lets you elide the check? No, the `(boxof symbol?)` contract has to be kept around because of mutability. Ah, right. Thanks. Robby _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Machinery for eliding contracts
On Mon, Jun 9, 2014 at 2:44 PM, Matthias Felleisen matth...@ccs.neu.edu wrote: On Jun 9, 2014, at 9:38 AM, Sam Tobin-Hochstadt sa...@cs.indiana.edu wrote: On Mon, Jun 9, 2014 at 3:19 AM, Eric Dobson eric.n.dob...@gmail.com wrote: It would be nice if the contract on the input to g could be elided. It seems like this could be done by using something like prop:contracted but that allowed accessing the parties that agreed to the contract. I'm imagining something like (lambda (v) (and (has-contract? v) (contracted-value-providing-side=? v 'the-typed-world) (contract-stronger? (value-contract v) new-contract))) One issue I see is that we need an unforgeable property that the value actually came from the typed world so we know that eliding the new contract is safe. Does this seem like a reasonable thing to support/do people see issues with it? It seems like this could be simplified a little just by allowing contract parties to be compared. IOW, at the point where you're writing that function, we have two contracts, and we need to know if the negative party of one is the positive party of the other. Then you don't need to worry about unforgeability, I think. Well some code could swap identities on such things. Not accidentally. Plus I think this would eliminate the anticipated benefits if there are chains of TR modules involved. I think Eric just needs to know whether something came out of the TR world and flows back w/o being touched. Yes I think this is what I want. TR should consider all typed modules as being the same. ;; --- Eric, are you talking about changing the proxy values that wrap HO/mutable contracted values? Yes. I want the proxy values to include information about who agreed to the contract in addition to the contract agreed to. I actually realize that I might need more than just the contract agreed to because of how TR changes the generated contract to remove checks for what it guarantees, so that info is not in the contract. But I believe that can be added back as a structure property on the contract. -- Matthias _ Racket Developers list: http://lists.racket-lang.org/dev
