Understanding vectorof: Q's on flatness, eager, immutable

Questions & Answers
1

When should vectorof be #:flat?

There is an option to declare a vectorof contract as flat. I believe this is because a vector might be mutated, but if your code is not supposed to be mutating the vector you can declare the contract flat to make testing faster? I feel like there's something I'm missing here.

Meaning of #:eager

I ordinarily think "eager" is the opposite of "lazy" - that is, do something right away instead of waiting. In the context of contracts, though, I don't understand where the deferred checking would occur. Doesn't it all need to be checked at the function boundary (at least if the function is invoked from another module)?

Is there another context besides define/contract where it makes more sense to defer the checking? What is it?

Immutable vs mutable - function vs not

With the immutable true option, the resulting contract is a function that can be applied to arguments. Not so when immutable is false. This is a surprise to me. Why is the behavior so different? There is no problem actually using the contract as a contract, but this surprised me while testing and I wanted to know if there was a simple explanation.

> ((vectorof integer? #:immutable #t) (vector-immutable 10 20 30))
#t
> ((vectorof integer? #:immutable #f) (vector-immutable 10 20 30))
application: not a procedure;
 expected a procedure that can be applied to arguments
  given: (vectorof integer? #:immutable #f)

Mutable struct vs vector

If you have a struct declared #:mutable, then there is no option to say "the contract is flat". That's different from vectors, right? Is there a reason? (Is it just "mutable-but-not-intended-to-be-mutated vectors are common"?)

2

(vectorof integer? #:immutable #f) is a chaperone contract; it's meant to wrap a vector and check vector-set! calls on it to check to see if the new value passes the element contract (integer? in this case). Chaperone contracts can't act like predicates the way flat contracts can.

(vectorof integer? #:flat? #t #:immutable #f) on the other hand, is a flat contract (And a chaperone contract at the same time somehow), but doesn't check vector-set!, making it unsafe as you can break the element contract:

(define/contract (foo v)
  (-> (vectorof integer? #:flat? #t #:immutable #f) void?)
  (vector-set! v 0 'a))

(define vec (vector 1 2 3))
(foo vec)
(println vec) ; '#(a 2 3)
(foo vec) ; contract violation

#:eager is used to conditionally control if the elements are checked when the vector is wrapped in a contract, or later when an element is accessed. It might be useful if you expect a function to be passed a large vector and only use a few elements of it.

(define/contract (foo v)
  (-> (vectorof integer? #:eager #f) void?)
  (println (vector-ref v 0)))

(define vec (vector 1 'a 3))
(foo vec) ; no contract violation!

I'm unfamiliar with struct contracts; I just wrap individual constructor/getter/setter functions in their own contracts in a contract-out clause of provide instead of using struct/c, struct/contract, etc.

3

Another to consider is that, because vectors can be mutable, there is deferred checking at the vector itself, sort of like how deferred checking at functions happens. In the case of functions, there isn't a sensible way to check "up front" like there is with a vector, so the situation isn't completely analogous. But, just because the vector, at the moment, has a value in it that satisfies the contract, that doesn't say anything about the future contents of the vector. So the lazy checking is checking on each access to the vector, not simply when the vector is returned from some function.

Here's some code to consider. If you leave the second printf commented out, there will be no contract violation. And, indeed, no problematic value has made its way into the client. But if you bring that second printf line into the program, then you'll see that bad value does indeed (almost) make its way into client and so the contract system signals the violation.

#lang racket

(module server racket
  (provide
   (contract-out
    [get-v (-> integer? (vectorof integer?))]
    [do-something-buggy (-> void?)]))

  (define v (vector 0))

  (define (get-v n)
    (vector-set! v 0 n)
    v)
  
  (define (do-something-buggy)
    (vector-set! v 0 "not an integer")))

(module client racket
  (require (submod ".." server))

  (define v (get-v 10))
  (printf "v[0]=~s\n" (vector-ref v 0))
  (do-something-buggy)
  ;(printf "v[0]=~s\n" (vector-ref v 0))
  )

(require 'client)

(as a more minor point, ever flat contract is a chaperone contract; this is more a matter of the definition or the terms than anything deep, however.)