[racket-dev] Machinery for eliding contracts

On Mon, Jun 9, 2014 at 2:44 PM, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
>
> On Jun 9, 2014, at 9:38 AM, Sam Tobin-Hochstadt <samth at cs.indiana.edu> wrote:
>
>> On Mon, Jun 9, 2014 at 3:19 AM, Eric Dobson <eric.n.dobson at 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
>
>
>