[racket-dev] Machinery for eliding contracts

From: Sam Tobin-Hochstadt (samth at cs.indiana.edu)
Date: Mon Jun 9 09:38:18 EDT 2014

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.

Sam

Posted on the dev mailing list.