[racket-dev] Contract barrier inefficiencies

1. Robby responded to your first item some time back. He and I had discussed contract-stronger and eq? check several times in the past. But even that doesn't assure improved checking w/o some performance-oriented thinking on the programmer's side. 

2. Sam didn't respond to the second part, which contained two questions. To answer the first one, I changed your code a bit. As for the second one, I think it is a lack os smarts but I am not sure this smarts can be exploited. See below, with modifications labeled MF. 

3. Because we anticipated performance distortions by contracts, Robby and I decided to make contracts a 'module' level tool. The hope was that Racket programmers would (1) trust themselves with their own code within a module ("No panic on the Titanic" was my slogan to remind ourselves of this argument; why choose an untyped language otherwise?) and (2) avoid 'tight' loops across module boundaries. 

Note: Since then we have learned that Racket programmers don't trust themselves; see the introduction of define/contract and friends and the repeated misunderstanding that this would check contracts even for internal recursive calls. We have also learned that in the context of generated contracts -- TR -- tight loops might show up. 

I am beginning to wonder whether the work on Optimization Coach should turn to this area next i.e. whether we should figure out a tool that anticipates potential performance problems in linked programs. As a stand-alone library racket/math clearly doesn't pose any problems. When linked into an untyped context, things might go wrong however -- as your toy benchmark shows. Or we just sit back and hope that nobody is ever bothered by this performance hit because 'realistic' programs won't suffer from this problem. 

-- Matthias



#lang racket

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

 (define (make-foo x) x)

 (define (foo? x)
   (printf "foo?~n")
   (exact-integer? x))
  
  ;; MF: manipulate foos behind your back 
  (define (set-foos v)
    (vector-set! v 5 (exact->inexact (vector-ref v 5))))
  
  ;; MF: make foos here 
  (define foos (build-vector 10 make-foo)))

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

 (require/typed
  (submod ".." foo-defs)
  [#:opaque Foo foo?]
  [make-foo (Integer -> Foo)]
  ;; MF: type foos properly 
  [foos (Vectorof Foo)] 
  ;; MF: promise the world here 
  [set-foos ((Vectorof Foo) -> Void)])

 ;; prints `foo?' 10 times; definitely necessary
 
 (: 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))
  
  (: bar-ap (All (A) ((Foo -> A) Integer -> A)))
 (define (bar-ap f foo)
   (f (get-foo foo))))

(require 'typed-defs 'foo-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")
(set-foos foos) ;; MF: this does NOT raise an error
(with-handlers ((exn:fail:contract:blame? void))
  (get-foo 5) ; prints `foo?' once; why? MF: because it could have been modified, despite the type 
  (displayln "ouch, it didn't catch the problem"))

; 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")
(with-handlers ((exn:fail:contract:blame? void))
  (foo-ap identity (exact->inexact (get-foo 1))))  ; prints `foo?' twice; why not once, just for 1?
;; MF: the first time because it might get a bad foo


(bar-ap identity 5)  ; prints `foo?' twice; why not once, just for 1?
;; MF: After some playing around, I don't know either. 
;; Conjecture: the translation of the All type does not take into account that no matter what (Foo -> A) is applied to a Foo 
;; -- statically typed for sure, and possibly protected with a contract