[racket-dev] TR: Five feature/limitation interactions conspire to drive mad

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 ⊥

-------------- next part --------------
#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)