Re: [racket-dev] A Const type constructor
At Tue, 31 Jul 2012 14:36:06 -0400, Matthias Felleisen wrote: > > On Jul 31, 2012, at 1:31 PM, Neil Toronto wrote: > > > To reiterate after my absence: I won't write a typed math/vector > > until using its exports in Typed Racket wouldn't be a huge friggin' > > PITA. > > Let me rephrase this ever so gently. Typed Racket has failed at least > one real test for now, namely, writing a highly usable math library. Agreed. The invariance of vectors is a pretty big usability problem here. > I think this is a fair judgment, and you are posing the obvious, not so > implied problem to the TR maintainers to fix this problem. They should > thank you on their knees, especially Vincent. Yes, Sam and I should fix this. Neil: I'll study your proposal in detail, and see how we could add it (or something similar) to TR. Thanks for taking the time to write it out. I'll have a look at what Scala does, too. AFAIK, they also have invariant vectors and more than one numeric type, so they probably have similar problems. > > To offer a carrot instead of a stick: There could be a short paper > > in this, titled "The Case for a Clean, Correct, Covariant Const". > > That is what I was thinking as I was reading your message. I have not > encountered such a proposal/language before, and I think it could be a > really neat extension of Vincent's PADL work. Agreed. > Perhaps the two of you > should work out the details together and submit follow-up to PADL > n+1. Oh never mind, D stands for declarative. So ship it to ICFP next > year, functional languages do include mutation. Sounds good to me. Neil: let's continue this discussion off-list. Vincent _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] A Const type constructor
On Jul 31, 2012, at 1:31 PM, Neil Toronto wrote: > To reiterate after my absence: I won't write a typed math/vector until using > its exports in Typed Racket wouldn't be a huge friggin' PITA. Let me rephrase this ever so gently. Typed Racket has failed at least one real test for now, namely, writing a highly usable math library. I think this is a fair judgment, and you are posing the obvious, not so implied problem to the TR maintainers to fix this problem. They should thank you on their knees, especially Vincent. > To offer a carrot instead of a stick: There could be a short paper in this, > titled "The Case for a Clean, Correct, Covariant Const". That is what I was thinking as I was reading your message. I have not encountered such a proposal/language before, and I think it could be a really neat extension of Vincent's PADL work. Perhaps the two of you should work out the details together and submit follow-up to PADL n+1. Oh never mind, D stands for declarative. So ship it to ICFP next year, functional languages do include mutation. -- Matthias smime.p7s Description: S/MIME cryptographic signature _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] A Const type constructor
On 07/25/2012 07:10 PM, D Herring wrote: On 07/25/2012 12:29 PM, Neil Toronto wrote: What if TR had a notion of const-ness, like in C? Suppose (Vectorof A) is a subtype of (Const-Vectorof B) when A is a subtype of B, and (Const-Vectorof A) is never a subtype of (Vectorof B). In C, "const" is a contract on the function type, not on the parameter data type. This can be a very useful contract. Once const applies to a variable, it becomes sticky and requires an explicit (and easily searched) const_cast downgrade to become mutable again. This can be useful and quite annoying. Using const in one spot often causes a snowball effect where it must be manually propagated to other function prototypes. C++ allows certain fields to be marked as mutable, even when the containing object is const. A more dynamic language might be able to decorate the value instead of the function, or at least infer const-ness where possible? Here's a possible way to make the "snowball"-ness less of an issue: have a Mutable constructor instead, and make (Vectorof A) mean (Const (Vectorof A)). Of course, that would mean functions should accept (Vectorof A) and return (Mutable (Vectorof A)), unless they actually return an immutable vector Here's a better idea. Let's say we want to type `vector-sqrt'. The best way using Const would be vector-sqrt : (Const (Vectorof Number)) -> (Vectorof Number) so that it could accept both kinds of vectors. If vectors were Const by default, it would be vector-sqrt : (Vectorof Number) -> (Mutable (Vectorof Number)) so that its return values could be used anywhere. What if, when a `Vectorof' were in an argument position, it was Const, and when in a return position, Mutable? The obvious type would be best: vector-sqrt : (Vectorof Number) -> (Vectorof Number) If a vector argument needed to be mutable, its type could be overridden: vector-set! : (All (a) (Mutable (Vectorof a)) Integer a -> Void) In the extremely rare case that a function returned an immutable vector, the return type could be overridden: vector->immutable-vector : (All (a) (Vectorof a) -> (Const (Vectorof a))) Making vector arguments Const by default could break existing code written in TR. I don't think a lot of code would break, though: 1. Racket is designed to discourage mutation. 2. Mutable data structures are hard to use in TR because they're not covariant, and ridiculously hard with numeric tower type parameters. 3. I found a nasty error: typed vector-ref indexes the wrong elements (often raising errors) on vectors from untyped code. I'm certain that because of this, there's no mixed typed/untyped code that uses vectors. To reiterate after my absence: I won't write a typed math/vector until using its exports in Typed Racket wouldn't be a huge friggin' PITA. To offer a carrot instead of a stick: There could be a short paper in this, titled "The Case for a Clean, Correct, Covariant Const". Neil ⊥ _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] A Const type constructor
On 07/25/2012 12:29 PM, Neil Toronto wrote: What if TR had a notion of const-ness, like in C? Suppose (Vectorof A) is a subtype of (Const-Vectorof B) when A is a subtype of B, and (Const-Vectorof A) is never a subtype of (Vectorof B). In C, "const" is a contract on the function type, not on the parameter data type. This can be a very useful contract. Once const applies to a variable, it becomes sticky and requires an explicit (and easily searched) const_cast downgrade to become mutable again. This can be useful and quite annoying. Using const in one spot often causes a snowball effect where it must be manually propagated to other function prototypes. C++ allows certain fields to be marked as mutable, even when the containing object is const. A more dynamic language might be able to decorate the value instead of the function, or at least infer const-ness where possible? - Daniel _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] A Const type constructor
On 07/25/2012 10:31 AM, Neil Toronto wrote: On 07/25/2012 10:26 AM, Sam Tobin-Hochstadt wrote: On Wed, Jul 25, 2012 at 9:29 AM, Neil Toronto wrote: After thinking about it, I don't want an Immutable-Vector type, for which v : Immutable-Vector proves (immutable? v) is #t. That would be seriously annoying to users of a vector library. What if TR had a notion of const-ness, like in C? Suppose (Vectorof A) is a subtype of (Const-Vectorof B) when A is a subtype of B, and (Const-Vectorof A) is never a subtype of (Vectorof B). How exactly are these different? An immutable vector is a vector, but could be covariant, which seems like what you want. However, a mutable vector can't be treated as an immutable vector. I don't want to tell Typed Racket "This vector's values never change." I want to tell it "Code in this scope never changes this vector's values." That's why I called it "const" instead of "immutable". To elaborate: an Immutable-Vector type would have these problems: * It would put a conversion burden on users. * It would be slow. Most vector-producing Racket functions produce mutable vectors. Users would have to convert them to immutable to get any decent use out of a math/vector library. I would want to convert them to immutable before returning them from functions, to decrease the burden on users. Conversion makes a copy: > (define x (vector 1 2 3)) > (eq? x (vector->immutable-vector x)) #f I can roll my own Immutable-Vector-like type right now, but it has exactly the same problems as immutable vectors; i.e. it puts a conversion burden on users and it's slow. I won't write a math/vector library until I can do better. The homebrew Immutable-Vector-like thing is a good way to illustrate what I'm asking for in a Const type constructor, though, so here it is. Suppose I want to write `vector=', which lifts `=' to operate pointwise on vectors using something similar to `vector-andmap'. Here's the type: (: vector= ((Vectorof Number) (Vectorof Number) -> Boolean)) Of course, this won't work out: (define xs (vector 1.0 2.0)) (define ys (vector 1 2)) ;(vector= xs ys) ; Won't type So I make a read-only "view" of vectors, with conversion functions: (struct: (A) const-vector ([length : Index] [fun : (Index -> A)])) (: vector->const-vector (All (A) ((Vectorof A) -> (const-vector A (: const-vector->vector (All (A) ((const-vector A) -> (Vectorof A Now I can write a wrapper for `vector=': (: const-vector= ((const-vector Number) (const-vector Number) -> Boolean)) (define (const-vector= v1 v2) (vector= (const-vector->vector v1) (const-vector->vector v2))) I could use it like this: (define x (vector->const-vector xs)) (define y (vector->const-vector ys)) (const-vector= x y) ; Types, and returns #t THIS NEXT PART IS CRITICAL. *I don't care* whether someone alters the vector that backs a const-vector: (vector-set! xs 0 2.0) (const-vector= x y) ; Returns #f now, but I don't care The only thing I care about is having a fast, flat, covariant collection type. But this one is very slow. Timings for 100,000,000 refs on my system (run in command-line Racket): vector-ref 270ms unsafe-vector-ref130ms const-vector-ref 1950ms unsafe-const-vector-ref 1350ms About 10x slower overall. This is unacceptable for a math library. Let's look at some other, worse options. First, huge case-> types: (: vector= (case-> ((Vectorof Integer) (Vectorof Integer) -> Boolean) ((Vectorof Float) (Vectorof Float) -> Boolean) ((Vectorof Float-Complex) (Vectorof Float-Complex) -> Boolean) ((Vectorof Exact-Number) (Vectorof Exact-Number) -> Boolean) ((Vectorof Exact-Rational) (Vectorof Exact-Rational) -> Boolean) ((Vectorof Real) (Vectorof Real) -> Boolean) ((Vectorof Number) (Vectorof Number) -> Boolean))) The function body takes 7 times longer to typecheck than it would with a single function type. It would actually be better to do a cartesian product of type parameters (so I can test a (Vectorof Integer) against a (Vectorof Float)), which takes 49 times longer. Ouch. A terrible option, which would be like not having a type system: (: vector= ((Vectorof Any) (Vectorof Any) -> Boolean)) Internally, `vector=' would use occurrence typing to make sure it compares only numbers. A Const type like (Const (Vectorof A)) would have the same properties as a (const-vector A). Its inhabitants would be covariant, flat collections. However, it would be *fast* because the const-ness would be a property checked statically by the type system instead of hacked in using the covariance of function return types. I've attached the `const-vector' definitions in case you want to doub
Re: [racket-dev] A Const type constructor
On 07/25/2012 10:26 AM, Sam Tobin-Hochstadt wrote: On Wed, Jul 25, 2012 at 9:29 AM, Neil Toronto wrote: After thinking about it, I don't want an Immutable-Vector type, for which v : Immutable-Vector proves (immutable? v) is #t. That would be seriously annoying to users of a vector library. What if TR had a notion of const-ness, like in C? Suppose (Vectorof A) is a subtype of (Const-Vectorof B) when A is a subtype of B, and (Const-Vectorof A) is never a subtype of (Vectorof B). How exactly are these different? An immutable vector is a vector, but could be covariant, which seems like what you want. However, a mutable vector can't be treated as an immutable vector. I don't want to tell Typed Racket "This vector's values never change." I want to tell it "Code in this scope never changes this vector's values." That's why I called it "const" instead of "immutable". Neil ⊥ _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] A Const type constructor
On Wed, Jul 25, 2012 at 9:29 AM, Neil Toronto wrote: > After thinking about it, I don't want an Immutable-Vector type, for which v > : Immutable-Vector proves (immutable? v) is #t. That would be seriously > annoying to users of a vector library. > > What if TR had a notion of const-ness, like in C? Suppose (Vectorof A) is a > subtype of (Const-Vectorof B) when A is a subtype of B, and (Const-Vectorof > A) is never a subtype of (Vectorof B). How exactly are these different? An immutable vector is a vector, but could be covariant, which seems like what you want. However, a mutable vector can't be treated as an immutable vector. -- sam th sa...@ccs.neu.edu _ Racket Developers list: http://lists.racket-lang.org/dev
[racket-dev] A Const type constructor
After thinking about it, I don't want an Immutable-Vector type, for which v : Immutable-Vector proves (immutable? v) is #t. That would be seriously annoying to users of a vector library. What if TR had a notion of const-ness, like in C? Suppose (Vectorof A) is a subtype of (Const-Vectorof B) when A is a subtype of B, and (Const-Vectorof A) is never a subtype of (Vectorof B). Then I could tell TR that my functions *can't use the possibly mutable vectors they get as a communication channel*. For example: vector+ : (Const-Vectorof Number) (Const-Vectorof Number) -> (Vectorof Number) Then (vector+ xs ys) would type if `xs' and `ys' were any kind of vector of numbers, immutable or not. It could be made more general, with Const as a type constructor: vector+ : (Const (Vectorof Number)) (Const (Vectorof Number)) -> (Vectorof Number) Also, vector-ref : All (a) ((Const (Vectorof a)) Integer -> a) vector-set! : All (a) ((Vectorof a) Integer a -> Void) vector : All (a) (a * -> (Vectorof a) vector-immutable : All (a) (a * -> (Const (Vectorof a)) bytes-ref : (Const Bytes) Integer -> Byte bytes-set! : Bytes Integer Integer -> Void (Const A) = A for Const A (e.g. Number, (Const (Vectorof B))) (struct: (a) const-wrap ([data : (Const (Vectorof a))])) (Const (const-wrap A)) = (const-wrap A) (struct: (a) wrap ([data : (Vectorof a)])) If v : (Const (wrap A)) then (wrap-data v) : (Const (Vectorof a)) (Const (Vectorof (Vectorof a))) = (Const (Vectorof (Const (Vectorof a Would this work? Am I thinking about it correctly in the first place? Neil ⊥ _ Racket Developers list: http://lists.racket-lang.org/dev
