On 12/28/2012 08:23 AM, Matthias Felleisen wrote:
On Dec 27, 2012, at 9:22 PM, Neil Toronto wrote:
Sorry it took so long to reply.
I applied the patch and verified that my example runs a *lot* faster (with
domain and range contracts identical, of course). Unfortunately, a similar test
using arrays isn't any faster. This is how the identity function for arrays is
defined in the test:
(: array-id (All (A) ((Array A) -> (Array A))))
(define (array-id arr) arr)
If we had macros for types, we might be able to write
(All (A) (let ((t (Array A))) (t -> t)))
The change doesn't help because the contracts for each instance of (Array A) in
the type aren't identical. Merging such contracts would be a great space
optimization in general, but I don't know whether it would make using
`math/array' from untyped code any faster.
Actually, right now, I'm sure it wouldn't help much. I can't think of any array
functions that return an array with an identical procedure
It is not an identical procedure that makes for contract optimizations here but
identical contracts/types. Would that help?
Hmm... it might, if the merging were thorough enough (i.e. merging
contracts from different modules) or `contract-stronger?' were used. By
the time an array is operated on in Typed Racket code, I think it's had
its procedure wrapped with two equivalent higher-order contracts. An
example:
#lang racket
(require math/array)
(define arr (make-array #(100 100) 0))
(array->mutable-array arr)
So `arr' has an (Array any/c) contract from being returned from
`make-array' across the barrier. When `array->mutable-array' operates on
it, it crosses the barrier again, so an (Array any/c) contract is applied.
What would be really nice is if passing the array back in to typed code
*removed* the contract put on it coming out, or removed parts of it. For
the array's procedure, the typed code needs a ((Vectorof Index) -> A).
It gets a value with the contract ((vectorof index?) . -> . any/c). The
typed code has been statically verified to not violate that contract.
Would it be sound for the barrier to detect that and unwrap the value?
Neil ⊥
On 12/18/2012 12:04 PM, Robby Findler wrote:
I can't help with the others, but for 1.) I've considered using a
contract-stronger? test or even just an eq? test when applying a
contract, checking what's already on the value. I haven't added that as
it hasn't come up "in anger" (and it isn't free, but the check is
cheap). If I put a broken test (diff below) and adjust your example a
little bit, it runs quickly for me. Does it also help in your larger
context?
Adjustment:
(module defs racket
(define c (any/c . -> . any/c))
(provide (contract-out [fun-id (-> c c)]))
(define (fun-id f) f))
Diff:
[robby@wireless-165-124-98-86] ~/git/plt/collects/racket$ git diff . | cat
diff --git a/collects/racket/contract/private/arrow.rkt
b/collects/racket/contract/private/arrow.rkt
index 55ed632..63c9a6e 100644
--- a/collects/racket/contract/private/arrow.rkt
+++ b/collects/racket/contract/private/arrow.rkt
@@ -506,6 +506,10 @@ v4 todo:
partial-mandatory-kwds
partial-optional-kwds
partial-ranges))
(λ (val)
+ (cond
+ [(eq? (value-contract val) ctc)
+ val]
+ [else
(if has-rest?
(check-procedure/more val mtd? dom-length
mandatory-keywords optional-keywords orig-blame)
(check-procedure val mtd? dom-length optionals-length
mandatory-keywords optional-keywords orig-blame))
@@ -521,7 +525,7 @@ v4 todo:
impersonator-prop:contracted ctc
impersonator-prop:application-mark (cons contract-key
;; is this right?
- partial-ranges)))))))
+
partial-ranges)))])))))
(define (->-name ctc)
(single-arrow-name-maker
The diff is broken because it doesn't account for blame. The test should
be making sure that the two contracts blame the same things
(alternatively, we could not check that and just drop the inner
contract. That may be better, but not as easy to try ...)
Robby
On Tue, Dec 18, 2012 at 12:06 PM, Neil Toronto <neil.toro...@gmail.com
<mailto:neil.toro...@gmail.com>> wrote:
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 ⊥
_________________________
Racket Developers list:
http://lists.racket-lang.org/__dev <http://lists.racket-lang.org/dev>
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
