[racket-dev] A very listy Typed Racket Integer

On 07/05/2012 05:54 PM, Sam Tobin-Hochstadt wrote:
> On Jul 5, 2012 8:50 PM, "Neil Toronto" <neil.toronto at gmail.com
> <mailto:neil.toronto at gmail.com>> wrote:
>  >
>  > (define-predicate boxof-integer? (Boxof Integer))
>
> This is the bug -- there's no way to write the boxof-integer? predicate,
> and define- predicate shouldn't think it can.

Meaning "no way that ensures preservation when some other piece of the 
program has a pointer to that box," right?

Anticipating a bug fix, I've started converting my recent TR code so 
that it doesn't define predicates for mutable container types. Instead 
of using `define-predicate', I need to *copy* the mutable data 
structure, using occurrence typing on each immutable containee. It's 
kind of a pain, but I only have one type that needs this treatment.

It's actually a good thing to have to do this. Copying happens at the 
boundary between private code and user code, and ensures that user code 
can't violate the private code's invariants by mutating private data.

If I had more to change, it'd be a major hassle. Would a 
`define-converter' be possible for mutable container types? Here's an 
example:

(define-converter (make-vectorof T) (Vectorof T))

#;(: make-vectorof (All (A B) ((A -> Boolean : B)
                                (Vectorof A) -> (U False (Vectorof B)))))
;; Receives a predicate that indicates `B' instances and a vector
;; Returns #f when every `A' in the vector isn't also a `B'

(: ds (Vectorof Integer))
(define ds (build-vector 10 identity))

(: idx-ds (U False (Vectorof Index)))
(define idx-ds (make-vectorof index? ds))  ; possibly makes a copy

(cond [idx-ds  ...]  ; idx-ds is a (Vectorof Index)
       [else  ...])   ; it's not


Of course, this wouldn't leverage the contract system nicely like 
define-predicate does.

I could also maintain invariants easily if I had an Immutable-Vectorof 
type. But that doesn't help with the fact that subtyping and occurrence 
typing don't work nicely on parameterized mutable types.

Neil ⊥