[racket-dev] Contract barrier inefficiencies

So there are potentially huge inefficiencies when mixing typed and 
untyped code, usually when functions are passed across the contract 
barrier. Here are a few things that I think cause them. Can the People 
Who Know This Stuff Really Well please comment on these issues?

====
1. Functions that cross the contract barrier can have exactly the same 
contract applied multiple times. Here's some benchmark code that 
demonstrates the issue:

#lang racket

(module defs racket
   (provide (contract-out [fun-id  (-> (any/c . -> . any/c)
                                       (any/c . -> . any/c))]))
   (define (fun-id f) f))

(require 'defs)

(define (f x) x)

(define h
   (for/fold ([h f]) ([_  (in-range 1000)])
     (fun-id h)))

(for ([_  (in-range 5)])
   (time (for ([_  (in-range 1000)])
           (h 5))))


I get over 800ms for each 1000 applications of `h', because it's 
basically a 1000-deep wrapper. (Or is it 2000?)

(The contract system is smart enough to check the contract quickly when 
the types are (any/c . -> . any), but I don't think TR ever generates 
contracts using `any'.)

This is a problem for `math/array' because array procedures are wrapped 
going in and going out with exactly the same contract: ((vectorof 
index?) . -> . any/c).

====
2. It seems TR checks more things than it really has to. In this 
example, the predicate `foo?' prints something so we can observe when 
it's applied, and is used as a predicate for an opaque type whose values 
cross the contract barrier:

#lang racket

;; Provides a predicate and constructor for the opaque type `Foo'
(module foo-defs racket
   (provide foo? make-foo)

   (define (make-foo x) x)

   (define (foo? x)
     (printf "foo?~n")
     (exact-integer? x))
   )

(module typed-defs typed/racket
   (provide get-foo foo-ap)

   (require/typed
    (submod ".." foo-defs)
    [#:opaque Foo foo?]
    [make-foo (Integer -> Foo)])

   ;; prints `foo?' 10 times; definitely necessary
   (define foos (build-vector 10 make-foo))

   (: get-foo (Integer -> Foo))
   (define (get-foo i)
     (vector-ref foos i))

   (: foo-ap (All (A) ((Foo -> A) Foo -> A)))
   (define (foo-ap f foo)
     (f foo))
   )

(require 'typed-defs)


I don't understand why the contract for `get-foo' has to check the 
return value, because TR already ensures that `get-foo' always returns a 
`Foo':

   (printf "going to get a foo~n")
   (get-foo 5)  ; prints `foo?' once; why?

Could TR generate (exact-integer? . -> . any) for `get-foo'?

Relatedly, TR already ensures that the function passed to `foo-ap' is 
only applied to `Foo' values, but this is also checked by a contract:

   (printf "going to apply a function to a foo~n")
   (foo-ap identity 1)  ; prints `foo?' twice; why not once, just for 1?

====
3. It's a shame we can't know statically whether an untyped function 
will return more than one value.

Suppose we could, and that TR generated contracts with `any/c' argument 
types for higher-order functions (i.e. fix issue #2). Then array 
procedures passed from untyped to typed code could have the contract 
(any/c . -> . any), which is checked immediately.

There's probably more, but this will do for now.

Neil ⊥