[racket-dev] Machinery for eliding contracts

On Mon, Jun 9, 2014 at 8: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.

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