[racket-dev] A very listy Typed Racket Integer

On 07/06/2012 09:11 AM, Sam Tobin-Hochstadt wrote:
> On Fri, Jul 6, 2012 at 11:59 AM, Neil Toronto <neil.toronto at gmail.com> wrote:
>> 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.

I can't maintain my invariants that way, because the same user code that 
sent the container might change the contained values.

>> (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'
>>
>> [...]
>
> I'm confused about what this does.  When does it copy, and when does
> it produce `#false`?

Here's a case where `make-vectorof' copies:

     (define ds (vector 0 1 2 3))
     (make-vectorof index? ds)

Here's a case where `make-vectorof' returns #f:

     ;; (expt 2 60) is not an Index on any platform:
     (define ds (vector (expt 2 60)))
     (make-vectorof index? ds)

>> 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 don't read `(make-vectorof index? ds)' as implicit.

It's generally true that mutable data is for sharing. But sometimes I 
don't intend to share mutable data; for example, when using a mutable 
data structure is a lot faster than using its functional counterpart. In 
that case, there's no way to follow basic user-interface guidelines for 
typing functions; i.e. to have general argument types and precise return 
types.

It's kind of a moot point now, anyway. I've decided to receive (Listof 
Integer) and return (Listof Index), and convert them to and from 
vectors. Lists will subtype nicely for my library users.

Neil ⊥