[racket-dev] Machinery for eliding contracts

From: Robby Findler (robby at eecs.northwestern.edu)
Date: Mon Jun 9 05:48:41 EDT 2014

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.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

Posted on the dev mailing list.