Re: [racket-dev] A very listy Typed Racket Integer
On Fri, Jul 6, 2012 at 11:59 AM, Neil Toronto neil.toro...@gmail.com wrote: On 07/05/2012 05:54 PM, Sam Tobin-Hochstadt wrote: On Jul 5, 2012 8:50 PM, Neil Toronto neil.toro...@gmail.com mailto:neil.toro...@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 sa...@ccs.neu.edu _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [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.toro...@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 ⊥ _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] A very listy Typed Racket Integer
On Jul 5, 2012 8:50 PM, Neil Toronto neil.toro...@gmail.com wrote: I just found this today: #lang typed/racket (define: b : (Boxof Any) (box 4)) (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. (define (set-b-box! v) (set-box! b v)) (: a-very-listy-integer (- Integer)) (define (a-very-listy-integer) (cond [(boxof-integer? b) (set-b-box! '(1 2 3)) (unbox b)] [else (error 'a-very-listy-integer can't happen)])) (a-very-listy-integer) - : Integer '(1 2 3) Is this a bug or a limitation? It can be replicated with any mutable container type as far as I can tell. A bug. Anytime you get a result like that it's a bug. Also, if it's a limitation, can I get (Vectorof Index) to be a subtype of (Vectorof Integer)? No, that relationship would be unsound for similar reasons. Neil ⊥ _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
