[racket-dev] A very listy Typed Racket Integer

On Fri, Jul 6, 2012 at 11:59 AM, Neil Toronto <neil.toronto at gmail.com> wrote:
> 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?

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.

Can you not do the checking *after* extracting the elements from the
container?  That may well be faster.

> 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

I'm confused about what this does.  When does it copy, and when does
it produce `#false`?

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

And in general, implicitly copying mutable data seems like a bad idea
-- mutable data is for sharing.

> 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.

Right.  Unfortunately, that's a pretty fundamental feature of
languages with mutation and aliasing.
-- 
sam th
samth at ccs.neu.edu