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
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
