[racket-dev] Machinery for eliding contracts

On Mon, Jun 9, 2014 at 5:48 AM, Robby Findler
<robby at 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.dobson at 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 200000)))
>>       (g (f 'x)))))
>>
>> (module user-2 typed/racket
>>   (provide go2)
>>   (require 'lib)
>>   (define (go2)
>>     (for ((i (in-range 100000000)))
>>       (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