[racket-dev] A Const type constructor

On 07/25/2012 10:31 AM, Neil Toronto wrote:
> On 07/25/2012 10:26 AM, Sam Tobin-Hochstadt wrote:
>> On Wed, Jul 25, 2012 at 9:29 AM, Neil Toronto <neil.toronto at gmail.com>
>> wrote:
>>> After thinking about it, I don't want an Immutable-Vector type, for
>>> which v
>>> : Immutable-Vector proves (immutable? v) is #t. That would be seriously
>>> annoying to users of a vector library.
>>>
>>> What if TR had a notion of const-ness, like in C? Suppose (Vectorof
>>> A) is a
>>> subtype of (Const-Vectorof B) when A is a subtype of B, and
>>> (Const-Vectorof
>>> A) is never a subtype of (Vectorof B).
>>
>> How exactly are these different?  An immutable vector is a vector, but
>> could be covariant, which seems like what you want. However, a mutable
>> vector can't be treated as an immutable vector.
>
> I don't want to tell Typed Racket "This vector's values never change." I
> want to tell it "Code in this scope never changes this vector's values."
> That's why I called it "const" instead of "immutable".

To elaborate: an Immutable-Vector type would have these problems:

  * It would put a conversion burden on users.
  * It would be slow.

Most vector-producing Racket functions produce mutable vectors. Users 
would have to convert them to immutable to get any decent use out of a 
math/vector library. I would want to convert them to immutable before 
returning them from functions, to decrease the burden on users. 
Conversion makes a copy:

   > (define x (vector 1 2 3))
   > (eq? x (vector->immutable-vector x))
   #f

I can roll my own Immutable-Vector-like type right now, but it has 
exactly the same problems as immutable vectors; i.e. it puts a 
conversion burden on users and it's slow.

I won't write a math/vector library until I can do better.

The homebrew Immutable-Vector-like thing is a good way to illustrate 
what I'm asking for in a Const type constructor, though, so here it is.

Suppose I want to write `vector=', which lifts `=' to operate pointwise 
on vectors using something similar to `vector-andmap'. Here's the type:

   (: vector= ((Vectorof Number) (Vectorof Number) -> Boolean))

Of course, this won't work out:

   (define xs (vector 1.0 2.0))
   (define ys (vector 1 2))
   ;(vector= xs ys)  ; Won't type

So I make a read-only "view" of vectors, with conversion functions:

   (struct: (A) const-vector ([length : Index] [fun : (Index -> A)]))

   (: vector->const-vector (All (A) ((Vectorof A) -> (const-vector A))))
   (: const-vector->vector (All (A) ((const-vector A) -> (Vectorof A))))

Now I can write a wrapper for `vector=':

   (: const-vector= ((const-vector Number) (const-vector Number)
                                           -> Boolean))
   (define (const-vector= v1 v2)
     (vector= (const-vector->vector v1) (const-vector->vector v2)))

I could use it like this:

   (define x (vector->const-vector xs))
   (define y (vector->const-vector ys))
   (const-vector= x y)  ; Types, and returns #t

THIS NEXT PART IS CRITICAL. *I don't care* whether someone alters the 
vector that backs a const-vector:

   (vector-set! xs 0 2.0)
   (const-vector= x y)  ; Returns #f now, but I don't care

The only thing I care about is having a fast, flat, covariant collection 
type. But this one is very slow. Timings for 100,000,000 refs on my 
system (run in command-line Racket):

   vector-ref               270ms
   unsafe-vector-ref        130ms
   const-vector-ref         1950ms
   unsafe-const-vector-ref  1350ms

About 10x slower overall. This is unacceptable for a math library.

Let's look at some other, worse options. First, huge case-> types:

   (: vector=
      (case-> ((Vectorof Integer) (Vectorof Integer) -> Boolean)
              ((Vectorof Float) (Vectorof Float) -> Boolean)
              ((Vectorof Float-Complex) (Vectorof Float-Complex)
                                        -> Boolean)
              ((Vectorof Exact-Number) (Vectorof Exact-Number)
                                       -> Boolean)
              ((Vectorof Exact-Rational) (Vectorof Exact-Rational)
                                         -> Boolean)
              ((Vectorof Real) (Vectorof Real) -> Boolean)
              ((Vectorof Number) (Vectorof Number) -> Boolean)))

The function body takes 7 times longer to typecheck than it would with a 
single function type. It would actually be better to do a cartesian 
product of type parameters (so I can test a (Vectorof Integer) against a 
(Vectorof Float)), which takes 49 times longer. Ouch.

A terrible option, which would be like not having a type system:

   (: vector= ((Vectorof Any) (Vectorof Any) -> Boolean))

Internally, `vector=' would use occurrence typing to make sure it 
compares only numbers.

A Const type like (Const (Vectorof A)) would have the same properties as 
a (const-vector A). Its inhabitants would be covariant, flat 
collections. However, it would be *fast* because the const-ness would be 
a property checked statically by the type system instead of hacked in 
using the covariance of function return types.

I've attached the `const-vector' definitions in case you want to 
double-check that I've made every effort to make const-vector-ref fast.

Neil ⊥

-------------- next part --------------
#lang typed/racket

(require racket/unsafe/ops)

;; Use instead of vector-ref to disable partial bounds checking elimination pessimization
(define :vector-ref vector-ref)

(: vector= ((Vectorof Number) (Vectorof Number) -> Boolean))
(define (vector= vs1 vs2)
  (define n (vector-length vs1))
  (cond [(= n (vector-length vs2))
         (let loop ([i 0])
           (cond [(i . < . n)  (and (= (vector-ref vs1 i) (vector-ref vs2 i))
                                    (loop (+ i 1)))]
                 [else  #t]))]
        [else  #f]))

(define xs (vector 1.0 2.0))
(define ys (vector 1 2))
;(vector= xs ys)  ; Won't type

;; So make a ref-only "view" struct for vectors; a vector is not mutable
;; through one of these (but is from anything that has a pointer to an original)
(struct: (A) const-vector ([length : Index] [fun : (Index -> A)]))

(: vector->const-vector (All (A) ((Vectorof A) -> (const-vector A))))
;; Convert from vector `vs' to a const-vector backed by `vs'
(define (vector->const-vector vs)
  (const-vector (vector-length vs) (λ: ([i : Index])
                                     ;; Will be bounds-checked by const-vector-ref
                                     (unsafe-vector-ref vs i))))

(: const-vector->vector (All (A) ((const-vector A) -> (Vectorof A))))
;; Convert from a const vector to a new vector
(define (const-vector->vector v)
  ;; Dunno why build-vector doesn't work here; it should according to its type
  (list->vector (build-list (const-vector-length v) (const-vector-fun v))))

(: const-vector= ((const-vector Number) (const-vector Number) -> Boolean))
;; Wrapper for vector=
(define (const-vector= v1 v2)
  (vector= (const-vector->vector v1) (const-vector->vector v2)))

(define x (vector->const-vector xs))
(define y (vector->const-vector ys))
(const-vector= x y)  ; Types, and returns #t

(vector-set! xs 0 2.0)
(const-vector= x y)  ; Returns #f now, but I don't care

(: unsafe-const-vector-ref (All (A) ((const-vector A) Index -> A)))
;; Unsafely returns element at i
(define (unsafe-const-vector-ref v i)
  ((const-vector-fun v) i))

(: const-vector-ref (All (A) ((const-vector A) Integer -> A)))
;; Returns element at i with bounds checking
(define (const-vector-ref v i)
  (cond [(and (0 . <= . i) (i . < . (const-vector-length v)))
         (unsafe-const-vector-ref v i)]
        [else  (raise-type-error 'const-vector-ref
                                 (format "Index < ~a" (const-vector-length v))
                                 1 v i)]))

;; Timing tests for 100,000,000 refs

(printf "100000000 vector-ref:~n")
;; Averages 270ms
(for ([_  (in-range 5)])
  (time (for ([_  (in-range 100000000)])
          (:vector-ref xs 0))))

(printf "100000000 unsafe-vector-ref:~n")
;; Averages 130ms
(for ([_  (in-range 5)])
  (time (for ([_  (in-range 100000000)])
          (unsafe-vector-ref xs 0))))

(printf "100000000 const-vector-ref:~n")
;; Averages 1950ms
(for ([_  (in-range 5)])
  (time (for ([_  (in-range 100000000)])
          (const-vector-ref x 0))))

(printf "100000000 unsafe-vector-ref:~n")
;; Averages 1350ms
(for ([_  (in-range 5)])
  (time (for ([_  (in-range 100000000)])
          (unsafe-const-vector-ref x 0))))