On 12/31/2012 02:56 PM, Vincent St-Amour wrote:
At Mon, 31 Dec 2012 13:27:50 -0700,
Neil Toronto wrote:
2. Don't generalize argument types in let loops.
This is a bad idea. Often, inferring the types of loops only works
because of type generalization.
Agreed. Since this one is only a problem because of the other
limitations you list, ideally we should fix the others and leave this
one alone. Do you agree?
Very yes.
3. Allow let: loops to have unannotated arguments and return values.
This would totally work. I could use [i : Nonnegative-Fixnum 0] instead
of [#{i : Nonnegative-Fixnum} 0], and still not have to annotate `acc'
or the loop's return value.
Trying this one right now.
Thanks again. :D
4. Extend the set of types TR can produce contracts for.
This probably only works for first-order function types. It would be
helpful, but may not even work for functions with `Array' or `Matrix'
arguments (they're higher-order).
I can look into making contract generation smarter. Could you send me
a list of types that caused you issues with contract generation?
Actual examples are attached as a standalone Typed Racket program, with
the function bodies stubbed out. I think they cover pretty much all the
uses of `require/untyped-contract' in the math library.
Neil ⊥
#lang typed/racket
(struct: (A) Array ())
(define-type Indexes (Vectorof Index))
(define-type In-Indexes (U Indexes (Vectorof Integer)))
;;
---------------------------------------------------------------------------------------------------
;; Changing argument types from In-Indexes to (Vectorof Integer)
;; Most uses of `require/untyped-contract' in `math/array' are for this.
(: make-array (All (A) (In-Indexes A -> (Array A))))
(define (make-array ds v)
(error 'undefined))
;; The contract can be created, but is ambiguous and always fails. Exported to
untyped Racket using
;; this subtype:
#;(All (A) ((Vectorof Integer) A -> (Array A)))
;;
---------------------------------------------------------------------------------------------------
;; array-map's type
;; There was no subtype of this under which I could export it to untyped code:
(: array-map (All (R A B T ...)
(case-> ((-> R) -> (Array R))
((A -> R) (Array A) -> (Array R))
((A B T ... T -> R) (Array A) (Array B) (Array T) ...
T -> (Array R)))))
(define array-map
(case-lambda
[(f) (error 'undefined)]
[(f arr) (error 'undefined)]
[(f arr0 arr1) (error 'undefined)]
[(f arr0 arr1 . arrs) (error 'undefined)]))
;; I ended up making a separate, typed implementation for untyped code, with
the type
#;(All (R A) (case-> ((-> R) -> (Array R))
((A -> R) (Array A) -> (Array R))
((A A A * -> R) (Array A) (Array A) (Array A) * -> (Array
R))))
;;
---------------------------------------------------------------------------------------------------
;; Matrix argument types
;; Almost all uses of `require/untyped-contract' in `math/matrix' are for this.
(: matrix-determinant (case-> ((Array Real) -> Real)
((Array Number) -> Number)))
(define (matrix-determinant M)
(error 'undefined))
;; Exported using the subtype
#;((Array Number) -> Number)
;;
---------------------------------------------------------------------------------------------------
;; First-order numeric functions
;; Almost all uses of `require/untyped-contract' in `math/number-theory' and
`math/special-functions'
;; are variations of the following:
(: factorial (case-> (Zero -> One)
(One -> One)
(Integer -> Positive-Integer)))
(define (factorial n)
(error 'undefined))
;; Exported using the subtype
#;(Integer -> Positive-Integer)
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
